--- a/src/HOL/Tools/groebner.ML Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Tools/groebner.ML Fri May 13 22:55:00 2011 +0200
@@ -1012,10 +1012,10 @@
THEN ring_tac add_ths del_ths ctxt 1
end
in
- clarify_tac @{claset} i
+ clarify_tac @{context} i
THEN Object_Logic.full_atomize_tac i
THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i
- THEN clarify_tac @{claset} i
+ THEN clarify_tac @{context} i
THEN (REPEAT (CONVERSION (#unwind_conv thy) i))
THEN SUBPROOF poly_exists_tac ctxt i
end