src/HOL/Tools/Qelim/cooper.ML
changeset 33037 b22e44496dc2
parent 33002 f3f02f36a3e2
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -308,7 +308,7 @@
     1.4    | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
     1.5    | _ => (acc, dacc)
     1.6    val (cs,ds) = h ([],[]) p
     1.7 -  val l = Integer.lcms (cs union ds)
     1.8 +  val l = Integer.lcms (gen_union (op =) (cs, ds))
     1.9    fun cv k ct =
    1.10      let val (tm as b$s$t) = term_of ct
    1.11      in ((HOLogic.eq_const bT)$tm$(b$(linear_cmul k s)$(linear_cmul k t))