--- a/ProgTutorial/Package/simple_inductive_package.ML	Sun Oct 04 21:56:53 2009 +0200
+++ b/ProgTutorial/Package/simple_inductive_package.ML	Mon Oct 05 11:45:49 2009 +0200
@@ -65,7 +65,7 @@
 fun induction_tac defs prems insts =
   EVERY1 [ObjectLogic.full_atomize_tac,
           cut_facts_tac prems,
-          K (rewrite_goals_tac defs),
+          rewrite_goal_tac defs,
           EVERY' (map (dtac o inst_spec) insts),
           assume_tac]
 (* @end *)
@@ -139,7 +139,7 @@
 
 fun introductions_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}]),
           subproof1 rules preds i ctxt]