--- a/src/HOL/Bali/Evaln.thy Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/Bali/Evaln.thy Mon Nov 10 21:49:48 2014 +0100
@@ -449,7 +449,7 @@
"G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w, s') \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> (w, s')"
apply (erule evaln.induct)
apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac @{thm Suc_le_D_lemma},
- REPEAT o smp_tac 1,
+ REPEAT o smp_tac @{context} 1,
resolve_tac @{thms evaln.intros} THEN_ALL_NEW TRY o atac]) *})
(* 3 subgoals *)
apply (auto split del: split_if)