src/HOL/IMPP/Natural.thy

 apply (best elim: evalc_WHILE_case)+
 done
 
 lemma evaln_evalc: "<c,s> -n-> t ==> <c,s> -c-> t"
 apply (erule evaln.induct)
-apply (tactic {* ALLGOALS (resolve_tac @{thms evalc.intros} THEN_ALL_NEW atac) *})
+apply (tactic {* ALLGOALS (resolve_tac @{context} @{thms evalc.intros} THEN_ALL_NEW atac) *})
 done
 
 lemma Suc_le_D_lemma: "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"
 apply (frule Suc_le_D)
 apply blast

 
 lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t"
 apply (erule evalc.induct)
 apply (tactic {* ALLGOALS (REPEAT o etac exE) *})
 apply (tactic {* TRYALL (EVERY' [dtac @{thm evaln_max2}, assume_tac @{context},
-  REPEAT o eresolve_tac [exE, conjE]]) *})
-apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *})
+  REPEAT o eresolve_tac @{context} [exE, conjE]]) *})
+apply (tactic
+  {* ALLGOALS (rtac exI THEN' resolve_tac @{context} @{thms evaln.intros} THEN_ALL_NEW atac) *})
 done
 
 lemma eval_eq: "<c,s> -c-> t = (? n. <c,s> -n-> t)"
 apply (fast elim: evalc_evaln evaln_evalc)
 done