src/HOL/Tools/Groebner_Basis/groebner.ML

--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Nov 24 17:28:25 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,Library.take (length qs, rs) ~~ vars)
+ in (eq,(uncurry take) (length qs, rs) ~~ vars)
  end;
  fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p));
 in