src/HOL/Tools/Groebner_Basis/groebner.ML

  let 
   val vars = filter (fn v => free_in v eq) evs
   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
  fun solve_idealism evs ps eqs =
   if null evs then [] else