diff -r c46910a6bfce -r 833d154ab189 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Wed Jan 31 21:05:47 2018 +0100
+++ b/src/HOL/Tools/groebner.ML	Thu Feb 01 13:55:10 2018 +0100
@@ -646,8 +646,7 @@
   val cjs = conjs tm
   val  rawvars =
     fold_rev (fn eq => fn a => grobvars (Thm.dest_arg1 eq) (grobvars (Thm.dest_arg eq) a)) cjs []
-  val vars = sort (fn (x, y) => Term_Ord.term_ord (Thm.term_of x, Thm.term_of y))
-                  (distinct (op aconvc) rawvars)
+  val vars = sort Thm.term_ord (distinct (op aconvc) rawvars)
  in (vars,map (grobify_equation vars) cjs)
  end;
 
@@ -866,8 +865,7 @@
  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) => Term_Ord.term_ord (Thm.term_of s, Thm.term_of t))
+  val rs = ideal (qs @ ps) p Thm.term_ord
  in (eq, take (length qs) rs ~~ vars)
  end;
  fun subst_in_poly i p = Thm.rhs_of (ring_normalize_conv (vsubst i p));