--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Thu Jun 28 19:09:35 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Thu Jun 28 19:09:36 2007 +0200
@@ -27,7 +27,7 @@
val denominator_rat = Rat.quotient_of_rat #> snd #> Rat.rat_of_int;
fun int_of_rat a =
case Rat.quotient_of_rat a of (i,1) => i | _ => error "int_of_rat: not an int";
-val lcm_rat = fn x => fn y => Rat.rat_of_int (lcm (int_of_rat x, int_of_rat y));
+val lcm_rat = fn x => fn y => Rat.rat_of_int (Integer.lcm (int_of_rat x) (int_of_rat y));
val (eqF_intr, eqF_elim) =
let val [th1,th2] = thms "PFalse"
--- a/src/HOL/Tools/Qelim/cooper.ML Thu Jun 28 19:09:35 2007 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Thu Jun 28 19:09:36 2007 +0200
@@ -311,7 +311,7 @@
| Const("Not",_)$_ => h (acc,dacc) (Thm.dest_arg t)
| _ => (acc, dacc)
val (cs,ds) = h ([],[]) p
- val l = fold (curry lcm) (cs union ds) 1
+ val l = fold Integer.lcm (cs union ds) 1
fun cv k ct =
let val (tm as b$s$t) = term_of ct
in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))
@@ -404,7 +404,7 @@
| NDvd (d,s) => (bacc,aacc,insert int_eq (term_of d|> dest_numeral) dacc)
| _ => (bacc, aacc, dacc)
val (b0,a0,ds) = h p ([],[],[])
- val d = fold (curry lcm) ds 1
+ val d = fold Integer.lcm ds 1
val cd = mk_cnumber @{ctyp "int"} d
val dt = term_of cd
fun divprop x =