int.ml.patch

1089c1089
<      (<) in
---
>      Term.(<) in
1819c1819
<   and upconv =
---
>   and upconv tm =
1822c1822
<       INT_POW_REM; INT_REM_REM] in
---
>       INT_POW_REM; INT_REM_REM] tm in
1826,1857d1825
< (* Reduction of (a pow k) rem n keeping intermediates reduced.               *)
< (* ------------------------------------------------------------------------- *)
< 
< let INT_POW_REM_CONV =
<   let pth_0,pth_1 = (CONJ_PAIR o prove)
<    (`((&m pow k) rem &n = &(m EXP k MOD n) /\
<       (&m pow k) rem (-- &n) = &(m EXP k MOD n)) /\
<      ((-- &m pow k) rem &n =
<       if EVEN k then &(m EXP k MOD n) else (-- &(m EXP k MOD n)) rem &n) /\
<      ((-- &m pow k) rem (-- &n) =
<       if EVEN k then &(m EXP k MOD n) else (-- &(m EXP k MOD n)) rem &n)`,
<     REWRITE_TAC[INT_REM_RNEG; INT_POW_NEG] THEN
<     COND_CASES_TAC THEN
<     ASM_REWRITE_TAC[GSYM INT_OF_NUM_CLAUSES; GSYM INT_OF_NUM_REM] THEN
<     CONV_TAC INT_REM_DOWN_CONV THEN REFL_TAC) in
<   let conv =
<     (GEN_REWRITE_CONV I [pth_0] THENC RAND_CONV EXP_MOD_CONV) ORELSEC
<     (GEN_REWRITE_CONV I [pth_1] THENC
<      RATOR_CONV(LAND_CONV NUM_EVEN_CONV) THENC
<      GEN_REWRITE_CONV I [COND_CLAUSES] THENC
<      (RAND_CONV EXP_MOD_CONV ORELSEC
<       (LAND_CONV
<        (RAND_CONV(RAND_CONV EXP_MOD_CONV THENC TRY_CONV INT_NEG_CONV)) THENC
<         INT_REM_CONV))) in
<   fun tm ->
<     match tm with
<       Comb(Comb(Const("rem",_),
<                 Comb(Comb(Const("int_pow",_),m),k)),n)
<       when is_intconst m && is_numeral k && is_intconst n -> conv tm
<   | _ -> failwith "INT_POW_REM_CONV";;
< 
< (* ------------------------------------------------------------------------- *)
2100c2068
<     let nim = setify(find_terms is_numimage bod) in
---
>     let nim = setify Term.(<) (find_terms is_numimage bod) in