--- a/ProgTutorial/Tactical.thy	Sun Oct 04 21:56:53 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Mon Oct 05 11:45:49 2009 +0200
@@ -1366,7 +1366,7 @@
 
   
   The simplifier is often used to unfold definitions in a proof. For this the
-  simplifier implements the tactic @{ML_ind  rewrite_goals_tac}.\footnote{FIXME: 
+  simplifier implements the tactic @{ML_ind  rewrite_goal_tac}.\footnote{\bf FIXME: 
   see LocalDefs infrastructure.} Suppose for example the
   definition
 *}
@@ -1374,12 +1374,11 @@
 definition "MyTrue \<equiv> True"
 
 text {*
-  then in the following proof we can unfold this constant
+  then we can use this tactic to unfold the definition of the constant.
 *}
 
-lemma shows "MyTrue \<Longrightarrow> True \<and> True"
-apply(rule conjI)
-apply(tactic {* rewrite_goals_tac @{thms MyTrue_def} *})
+lemma shows "MyTrue \<Longrightarrow> True"
+apply(tactic {* rewrite_goal_tac @{thms MyTrue_def} 1 *})
 txt{* producing the goal state
 
       \begin{minipage}{\textwidth}
@@ -1388,7 +1387,8 @@
 (*<*)oops(*>*)
 
 text {*
-  As you can see, the tactic unfolds the definitions in all subgoals.
+  If you want to unfold definitions in all subgoals, then use the 
+  the tactic @{ML_ind rewrite_goals_tac}.
 *}