changeset 33957 | e9afca2118d4 |
parent 33955 | fff6f11b1f09 |
child 35408 | b48ab741683b |
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Nov 24 17:28:44 2009 +0100 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Nov 25 09:13:46 2009 +0100 @@ -899,7 +899,7 @@ val (qs,p) = isolate_monomials vars eq val rs = ideal (qs @ ps) p (fn (s,t) => TermOrd.term_ord (term_of s, term_of t)) - in (eq,(uncurry take) (length qs, rs) ~~ vars) + in (eq, take (length qs) rs ~~ vars) end; fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p)); in