--- a/src/HOL/Bali/AxSem.thy Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Bali/AxSem.thy Tue Feb 10 14:48:26 2015 +0100
@@ -672,7 +672,7 @@
(* 37 subgoals *)
prefer 18 (* Methd *)
apply (rule ax_derivs.Methd, drule spec, erule mp, fast)
-apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros})) *})
+apply (tactic {* TRYALL (resolve_tac @{context} ((funpow 5 tl) @{thms ax_derivs.intros})) *})
apply auto
done
@@ -691,7 +691,7 @@
"G,(A::'a triple set)|\<turnstile>(ts'::'a triple set) \<Longrightarrow> !ts. ts \<subseteq> ts' \<longrightarrow> G,A|\<turnstile>ts"
apply (erule ax_derivs.induct)
(*42 subgoals*)
-apply (tactic "ALLGOALS strip_tac")
+apply (tactic "ALLGOALS (strip_tac @{context})")
apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD},
etac disjE, fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*})
apply (tactic "TRYALL (hyp_subst_tac @{context})")
@@ -703,7 +703,7 @@
apply (fast intro: ax_derivs.weaken)
apply (rule ax_derivs.conseq, clarify, tactic "smp_tac @{context} 3 1", blast(* unused *))
(*37 subgoals*)
-apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros})
+apply (tactic {* TRYALL (resolve_tac @{context} ((funpow 5 tl) @{thms ax_derivs.intros})
THEN_ALL_NEW fast_tac @{context}) *})
(*1 subgoal*)
apply (clarsimp simp add: subset_mtriples_iff)