--- a/src/HOL/Bali/AxSem.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/Bali/AxSem.thy Fri May 13 22:55:00 2011 +0200
@@ -661,7 +661,7 @@
lemma ax_thin [rule_format (no_asm)]:
"G,(A'::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A|\<turnstile>ts"
apply (erule ax_derivs.induct)
-apply (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])")
+apply (tactic "ALLGOALS (EVERY'[clarify_tac @{context}, REPEAT o smp_tac 1])")
apply (rule ax_derivs.empty)
apply (erule (1) ax_derivs.insert)
apply (fast intro: ax_derivs.asm)
@@ -692,7 +692,7 @@
(*42 subgoals*)
apply (tactic "ALLGOALS strip_tac")
apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD},
- etac disjE, fast_tac (@{claset} addSIs @{thms ax_derivs.empty})]))*})
+ etac disjE, fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*})
apply (tactic "TRYALL hyp_subst_tac")
apply (simp, rule ax_derivs.empty)
apply (drule subset_insertD)
@@ -703,7 +703,7 @@
apply (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
(*37 subgoals*)
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros})
- THEN_ALL_NEW fast_tac @{claset}) *})
+ THEN_ALL_NEW fast_tac @{context}) *})
(*1 subgoal*)
apply (clarsimp simp add: subset_mtriples_iff)
apply (rule ax_derivs.Methd)