--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Oct 21 12:02:19 2009 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Oct 21 12:02:56 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 =) (union (op =) (map fst lis1, 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)