diff -r 85fb70b0c5e8 -r 88bee9f6eec7 src/HOL/NanoJava/AxSem.thy
--- 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)