--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Oct 21 16:41:22 2009 +1100
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Oct 21 08:16:25 2009 +0200
@@ -348,7 +348,7 @@
| 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)
@@ -884,7 +884,7 @@
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