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