diff -r be361e980acf -r 82c482467d75 ProgTutorial/Tactical.thy --- 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 \ 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]}