# HG changeset patch
# User wenzelm
# Date 1369062677 -7200
# Node ID fcb40cadc1734e9f4fe8f334dbe27a002c3deed0
# Parent  5534ec8b90a91955a7f23ff339b2df590a0c1aa7
proper run-time context;

diff -r 5534ec8b90a9 -r fcb40cadc173 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Mon May 20 17:10:33 2013 +0200
+++ b/src/HOL/Tools/groebner.ML	Mon May 20 17:11:17 2013 +0200
@@ -1002,6 +1002,8 @@
  | _=> raise CTERM ("ideal_tac - lhs",[t])
  fun exitac NONE = no_tac
    | exitac (SOME y) = rtac (instantiate' [SOME (ctyp_of_term y)] [NONE,SOME y] exI) 1
+
+ val claset = claset_of @{context}
 in
 fun ideal_tac add_ths del_ths ctxt =
   presimplify ctxt add_ths del_ths
@@ -1023,10 +1025,10 @@
         THEN ring_tac add_ths del_ths ctxt 1
    end
   in
-     clarify_tac @{context} i
+     clarify_tac (put_claset claset ctxt) i
      THEN Object_Logic.full_atomize_tac i
      THEN asm_full_simp_tac (put_simpset (#poly_eq_ss thy) ctxt) i
-     THEN clarify_tac @{context} i
+     THEN clarify_tac (put_claset claset ctxt) i
      THEN (REPEAT (CONVERSION (#unwind_conv thy ctxt) i))
      THEN SUBPROOF poly_exists_tac ctxt i
   end