--- a/src/HOL/IMPP/Misc.thy Sun Nov 09 20:49:28 2014 +0100
+++ b/src/HOL/IMPP/Misc.thy Mon Nov 10 21:49:48 2014 +0100
@@ -71,12 +71,12 @@
apply (simp (no_asm_use) add: triple_valid_def2)
apply clarsimp
apply (drule_tac x = "s<Y>" in spec)
-apply (tactic "smp_tac 1 1")
+apply (tactic "smp_tac @{context} 1 1")
apply (drule spec)
apply (drule_tac x = "s[Loc Y::=a s]" in spec)
apply (simp (no_asm_use))
apply (erule (1) notE impE)
-apply (tactic "smp_tac 1 1")
+apply (tactic "smp_tac @{context} 1 1")
apply simp
done