--- a/ProgTutorial/Package/Ind_Code.thy	Sat Aug 31 08:07:45 2013 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Sun Dec 15 23:49:05 2013 +0000
@@ -253,10 +253,10 @@
   be implemented as follows:
 *}
 
-ML %linenosgray{*fun ind_tac defs prem insts =
-  EVERY1 [Object_Logic.full_atomize_tac,
+ML %linenosgray{*fun ind_tac ctxt defs prem insts =
+  EVERY1 [Object_Logic.full_atomize_tac ctxt,
           cut_facts_tac prem,
-          rewrite_goal_tac defs,
+          rewrite_goal_tac ctxt defs,
           inst_spec_tac insts,
           assume_tac]*}
 
@@ -277,7 +277,7 @@
 lemma automatic_ind_prin_even:
 assumes prem: "even z"
 shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P z"
-by (tactic {* ind_tac eo_defs @{thms prem} 
+by (tactic {* ind_tac @{context} eo_defs @{thms prem} 
                     [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}] *})
 
 lemma automatic_ind_prin_fresh:
@@ -286,7 +286,7 @@
         (\<And>a t s. \<lbrakk>P a t; P a s\<rbrakk> \<Longrightarrow> P a (App t s)) \<Longrightarrow>
         (\<And>a t. P a (Lam a t)) \<Longrightarrow> 
         (\<And>a b t. \<lbrakk>a \<noteq> b; P a t\<rbrakk> \<Longrightarrow> P a (Lam b t)) \<Longrightarrow> P z za"
-by (tactic {* ind_tac @{thms fresh_def} @{thms prem} 
+by (tactic {* ind_tac @{context} @{thms fresh_def} @{thms prem} 
                           [@{cterm "P::string\<Rightarrow>trm\<Rightarrow>bool"}] *})
 
 
@@ -340,7 +340,7 @@
          (srules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
 in
   Goal.prove lthy' [] [prem] goal
-      (fn {prems, ...} => ind_tac defs prems cnewpreds)
+      (fn {prems, context, ...} => ind_tac context defs prems cnewpreds)
   |> singleton (Proof_Context.export lthy' lthy)
 end *}
 
@@ -539,9 +539,9 @@
   will use the tactic
 *}
 
-ML %linenosgray{*fun expand_tac defs =
-  Object_Logic.rulify_tac 1
-  THEN rewrite_goal_tac defs 1
+ML %linenosgray{*fun expand_tac ctxt defs =
+  Object_Logic.rulify_tac ctxt 1
+  THEN rewrite_goal_tac ctxt defs 1
   THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}
 
 text {*
@@ -554,7 +554,7 @@
 lemma fresh_Lam:
 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
 (*>*)
-apply(tactic {* expand_tac @{thms fresh_def} *})
+apply(tactic {* expand_tac @{context} @{thms fresh_def} *})
 
 txt {*
   gives us the goal state
@@ -645,7 +645,7 @@
 (*<*)
 lemma fresh_Lam:
 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
-apply(tactic {* expand_tac @{thms fresh_def} *})
+apply(tactic {* expand_tac @{context} @{thms fresh_def} *})
 (*>*)
 apply(tactic {* chop_test_tac [fresh_pred] fresh_rules @{context} 1 *})
 (*<*)oops(*>*)
@@ -692,7 +692,7 @@
     val (params1, params2) = chop (length cparams - length preds) cparams
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
-    rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1
+    rtac (Object_Logic.rulify context (all_elims params1 (nth prems2 i))) 1
   end) *}
 
 text {* 
@@ -706,7 +706,7 @@
 (*<*)
 lemma fresh_Lam:
 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
-apply(tactic {* expand_tac @{thms fresh_def} *})
+apply(tactic {* expand_tac @{context} @{thms fresh_def} *})
 (*>*)
 apply(tactic {* apply_prem_tac 3 [fresh_pred] fresh_rules @{context} 1 *})
 (*<*)oops(*>*)
@@ -759,13 +759,13 @@
 *}
 
 ML %grayML{*fun prove_intro_tac i preds rules =
-  SUBPROOF (fn {params, prems, ...} =>
+  SUBPROOF (fn {params, prems, context, ...} =>
   let
     val cparams = map snd params
     val (params1, params2) = chop (length cparams - length preds) cparams
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
-    rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1
+    rtac (Object_Logic.rulify context (all_elims params1 (nth prems2 i))) 1
     THEN EVERY1 (map (prepare_prem params2 prems2) prems1)
   end) *}
 
@@ -776,7 +776,7 @@
 
 lemma fresh_Lam:
 shows "\<And>a b t. \<lbrakk>a \<noteq> b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
-apply(tactic {* expand_tac @{thms fresh_def} *})
+apply(tactic {* expand_tac @{context} @{thms fresh_def} *})
 apply(tactic {* prove_intro_tac 3 [fresh_pred] fresh_rules @{context} 1 *})
 done
 
@@ -793,7 +793,7 @@
 
 lemma accpartI:
 shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
-apply(tactic {* expand_tac @{thms accpart_def} *})
+apply(tactic {* expand_tac @{context} @{thms accpart_def} *})
 apply(tactic {* chop_test_tac [acc_pred] acc_rules @{context} 1 *})
 apply(tactic {* apply_prem_tac 0 [acc_pred] acc_rules @{context} 1 *})
 
@@ -864,7 +864,7 @@
     val (params1, params2) = chop (length cparams - length preds) cparams
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
-    rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1
+    rtac (Object_Logic.rulify context (all_elims params1 (nth prems2 i))) 1
     THEN EVERY1 (map (prepare_prem params2 prems2 context) prems1)
   end) *}
 
@@ -875,7 +875,7 @@
 
 lemma accpartI:
 shows "\<And>R x. (\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
-apply(tactic {* expand_tac @{thms accpart_def} *})
+apply(tactic {* expand_tac @{context} @{thms accpart_def} *})
 apply(tactic {* prove_intro_tac 0 [acc_pred] acc_rules @{context} 1 *})
 done
 
@@ -885,8 +885,8 @@
 *}
 
 ML %linenosgray{*fun intro_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}]),
           prove_intro_tac i preds rules ctxt]*}