src/HOL/Tools/Qelim/cooper.ML

   | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   | 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))
          |> HOLogic.mk_Trueprop |> provelin ctxt) RS eq_reflection end
   fun nzprop x =