--- a/ProgTutorial/Tactical.thy	Sat Aug 31 08:07:45 2013 +0100
+++ b/ProgTutorial/Tactical.thy	Sun Dec 15 23:49:05 2013 +0000
@@ -1574,7 +1574,7 @@
 
 lemma 
   shows "MyTrue \<Longrightarrow> True"
-apply(tactic {* rewrite_goal_tac @{thms MyTrue_def} 1 *})
+apply(tactic {* rewrite_goal_tac @{context} @{thms MyTrue_def} 1 *})
 txt{* producing the goal state
       \begin{isabelle}
       @{subgoals [display]}