diff -r a3793600cb93 -r 4d3527b94f2a src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/groebner.ML	Sun Dec 13 21:56:15 2015 +0100
@@ -970,7 +970,7 @@
      val cfs = (map swap o #multi_ideal thy evs ps)
                    (map Thm.dest_arg1 (conjuncts bod))
      val ws = map (exitac ctxt o AList.lookup op aconvc cfs) evs
-    in EVERY (rev ws) THEN Method.insert_tac prems 1
+    in EVERY (rev ws) THEN Method.insert_tac ctxt prems 1
         THEN ring_tac add_ths del_ths ctxt 1
    end
   in