src/HOL/Tools/Groebner_Basis/groebner.ML

         let val lis = resolve_proof vars lin in
             map (fn (n,p) => (n,grob_cmul pol p)) lis end
   | Add(lin1,lin2) =>
         let val lis1 = resolve_proof vars lin1
             val lis2 = resolve_proof vars lin2
-            val dom = distinct (op =) ((map fst lis1) union (map fst lis2))
+            val dom = distinct (op =) (union (op =) (map fst lis1, map fst lis2))
         in
             map (fn n => let val a = these (AList.lookup (op =) lis1 n)
                              val b = these (AList.lookup (op =) lis2 n)
                          in (n,grob_add a b) end) dom end;
 

   end
 
  fun isolate_monomials vars tm =
  let 
   val (cmons,vmons) =
-    List.partition (fn m => null (gen_inter op aconvc (frees m, vars)))
+    List.partition (fn m => null (inter op aconvc (frees m, vars)))
                    (striplist ring_dest_add tm)
   val cofactors = map (fn v => find_multipliers v vmons) vars
   val cnc = if null cmons then zero_tm
              else Thm.capply ring_neg_tm
                     (list_mk_binop ring_add_tm cmons)