diff -r 5f898411ce87 -r 5e94dfead1c2 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Wed Sep 09 14:47:41 2015 +0200
+++ b/src/HOL/Tools/groebner.ML	Wed Sep 09 20:57:21 2015 +0200
@@ -778,17 +778,20 @@
  in Conv.fconv_rule (Conv.arg_conv (Conv.arg1_conv ring_normalize_conv))
      (Thm.instantiate' [] [SOME a, SOME b] idl_sub)
  end
- val poly_eq_simproc =
+
+val poly_eq_simproc =
   let
-   fun proc phi ctxt t =
-    let val th = poly_eq_conv t
-    in if Thm.is_reflexive th then NONE else SOME th
-    end
-   in make_simproc {lhss = [Thm.lhs_of idl_sub],
-                name = "poly_eq_simproc", proc = proc, identifier = []}
-   end;
- val poly_eq_ss =
-   simpset_of (put_simpset HOL_basic_ss @{context}
+    fun proc ct =
+      let val th = poly_eq_conv ct
+      in if Thm.is_reflexive th then NONE else SOME th end
+  in
+    Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) "poly_eq_simproc"
+     {lhss = [Thm.term_of (Thm.lhs_of idl_sub)],
+      proc = fn _ => fn _ => proc, identifier = []}
+  end;
+
+val poly_eq_ss =
+  simpset_of (put_simpset HOL_basic_ss @{context}
     addsimps @{thms simp_thms}
     addsimprocs [poly_eq_simproc])