--- a/ProgTutorial/Package/Ind_Code.thy	Sun Oct 04 21:56:53 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Mon Oct 05 11:45:49 2009 +0200
@@ -278,7 +278,7 @@
 ML %linenosgray{*fun ind_tac defs prem insts =
   EVERY1 [ObjectLogic.full_atomize_tac,
           cut_facts_tac prem,
-          K (rewrite_goals_tac defs),
+          rewrite_goal_tac defs,
           inst_spec_tac insts,
           assume_tac]*}
 
@@ -563,7 +563,7 @@
 
 ML %linenosgray{*fun expand_tac defs =
   ObjectLogic.rulify_tac 1
-  THEN rewrite_goals_tac defs
+  THEN rewrite_goal_tac defs 1
   THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}
 
 text {*
@@ -905,7 +905,7 @@
 
 ML %linenosgray{*fun intro_tac defs rules preds i ctxt =
   EVERY1 [ObjectLogic.rulify_tac,
-          K (rewrite_goals_tac defs),
+          rewrite_goal_tac defs,
           REPEAT o (resolve_tac [@{thm allI}, @{thm impI}]),
           prove_intro_tac i preds rules ctxt]*}