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