src/HOL/Tools/Groebner_Basis/groebner.ML
changeset 33049 c38f02fdf35d
parent 33039 5018f6a76b3f
child 33050 fe166e8b9f07
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 10:15:31 2009 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 12:09:37 2009 +0200
@@ -884,7 +884,7 @@
  fun isolate_monomials vars tm =
  let 
   val (cmons,vmons) =
-    List.partition (fn m => null (inter op aconvc (frees m, vars)))
+    List.partition (fn m => null (inter (op aconvc) vars (frees m)))
                    (striplist ring_dest_add tm)
   val cofactors = map (fn v => find_multipliers v vmons) vars
   val cnc = if null cmons then zero_tm