--- a/ProgTutorial/Package/simple_inductive_package.ML	Sat Aug 31 08:07:45 2013 +0100
+++ b/ProgTutorial/Package/simple_inductive_package.ML	Sun Dec 15 23:49:05 2013 +0000
@@ -62,10 +62,10 @@
   Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec};
 
 (* @chunk induction_tac *)
-fun induction_tac defs prems insts =
-  EVERY1 [Object_Logic.full_atomize_tac,
+fun induction_tac ctxt defs prems insts =
+  EVERY1 [Object_Logic.full_atomize_tac ctxt,
           cut_facts_tac prems,
-          rewrite_goal_tac defs,
+          rewrite_goal_tac ctxt defs,
           EVERY' (map (dtac o inst_spec) insts),
           assume_tac]
 (* @end *)
@@ -96,7 +96,7 @@
          (rules', HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
   in
     Goal.prove lthy4 [] [prem] goal
-      (fn {prems, ...} => induction_tac defs prems cnewpreds)
+      (fn {prems, context, ...} => induction_tac context defs prems cnewpreds)
       |> singleton (Proof_Context.export lthy4 lthy1)
   end 
 in
@@ -131,15 +131,15 @@
     val (prems1, prems2) = chop (length prems - length rules) prems;
     val (params1, params2) = chop (length params - length preds) (map snd params);
   in
-    rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1 
+    rtac (Object_Logic.rulify ctxt' (all_elims params1 (nth prems2 i))) 1 
     THEN
     EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
   end)
 (* @end *)
 
 fun introductions_tac defs rules preds i ctxt =
-  EVERY1 [Object_Logic.rulify_tac,
-          rewrite_goal_tac defs,
+  EVERY1 [Object_Logic.rulify_tac ctxt,
+          rewrite_goal_tac ctxt defs,
           REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
           subproof1 rules preds i ctxt]