diff -r 2c34c69236ce -r 3c214b215f7e ProgTutorial/Tactical.thy --- 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 \ True" -apply(tactic {* print_tac "foo message" *}) +apply(tactic {* print_tac @{context} "foo message" *}) txt{*gives: \begin{isabelle} @{text "foo message"}\\[3mm]