# HG changeset patch
# User haftmann
# Date 1183050576 -7200
# Node ID 25e69e56355d83feebf6a7814f3fd3e0bbead3f2
# Parent  2ebb50c0db4f481efa0e7fda4fa166ea3d489913
dropped Library.lcm

diff -r 2ebb50c0db4f -r 25e69e56355d src/HOL/Tools/Groebner_Basis/groebner.ML
--- 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"
diff -r 2ebb50c0db4f -r 25e69e56355d src/HOL/Tools/Qelim/cooper.ML
--- 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 =