src/HOL/Tools/Groebner_Basis/groebner.ML
changeset 33050 fe166e8b9f07
parent 33042 ddf1f03a9ad9
parent 33049 c38f02fdf35d
child 33063 4d462963a7db
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 12:08:52 2009 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 12:12:21 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