ProgTutorial/Tactical.thy
changeset 556 3c214b215f7e
parent 554 638ed040e6f8
child 559 ffa5c4ec9611
--- a/ProgTutorial/Tactical.thy	Sun Apr 06 12:45:54 2014 +0100
+++ b/ProgTutorial/Tactical.thy	Wed May 28 12:41:09 2014 +0100
@@ -388,7 +388,7 @@
  
 lemma 
   shows "False \<Longrightarrow> True"
-apply(tactic {* print_tac "foo message" *})
+apply(tactic {* print_tac @{context} "foo message" *})
 txt{*gives:
      \begin{isabelle}
      @{text "foo message"}\\[3mm]