--- a/src/HOL/NanoJava/AxSem.thy Fri May 13 16:03:03 2011 +0200
+++ b/src/HOL/NanoJava/AxSem.thy Fri May 13 22:55:00 2011 +0200
@@ -151,7 +151,7 @@
"(A' |\<turnstile> C \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A |\<turnstile> C )) \<and>
(A' \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}))"
apply (rule hoare_ehoare.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 (blast intro: hoare_ehoare.Skip)
apply (blast intro: hoare_ehoare.Comp)
apply (blast intro: hoare_ehoare.Cond)