changeset 33039 | 5018f6a76b3f |
parent 33035 | 15eab423e573 |
parent 33038 | 8f9594c31de4 |
child 33042 | ddf1f03a9ad9 |
--- a/src/HOL/Tools/Qelim/cooper.ML Wed Oct 21 16:41:22 2009 +1100 +++ b/src/HOL/Tools/Qelim/cooper.ML Wed Oct 21 08:16:25 2009 +0200 @@ -308,7 +308,7 @@ | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t) | _ => (acc, dacc) val (cs,ds) = h ([],[]) p - val l = Integer.lcms (cs union ds) + val l = Integer.lcms (union (op =) (cs, ds)) 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))