src/HOL/Tools/Function/induction_schema.ML

 datatype ind_scheme = IndScheme of
  {T: typ, (* sum of products *)
   branches: scheme_branch list,
   cases: scheme_case list}
 
-val ind_atomize = Raw_Simplifier.rewrite true @{thms induct_atomize}
-val ind_rulify = Raw_Simplifier.rewrite true @{thms induct_rulify}
+fun ind_atomize ctxt = Raw_Simplifier.rewrite ctxt true @{thms induct_atomize}
+fun ind_rulify ctxt = Raw_Simplifier.rewrite ctxt true @{thms induct_rulify}
 
 fun meta thm = thm RS eq_reflection
 
-val sum_prod_conv = Raw_Simplifier.rewrite true
+fun sum_prod_conv ctxt = Raw_Simplifier.rewrite ctxt true
   (map meta (@{thm split_conv} :: @{thms sum.cases}))
 
 fun term_conv thy cv t =
   cv (cterm_of thy t)
   |> prop_of |> Logic.dest_equals |> snd

   in
     map f cases
   end
 
 
-fun mk_ind_goal thy branches =
-  let
+fun mk_ind_goal ctxt branches =
+  let
+    val thy = Proof_Context.theory_of ctxt
+
     fun brnch (SchemeBranch { P, xs, ws, Cs, ... }) =
       HOLogic.mk_Trueprop (list_comb (P, map Free xs))
       |> fold_rev (curry Logic.mk_implies) Cs
       |> fold_rev (Logic.all o Free) ws
-      |> term_conv thy ind_atomize
+      |> term_conv thy (ind_atomize ctxt)
       |> Object_Logic.drop_judgment thy
       |> HOLogic.tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
   in
     SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
   end
 
 fun mk_induct_rule ctxt R x complete_thms wf_thm ineqss
   (IndScheme {T, cases=scases, branches}) =
   let
+    val thy = Proof_Context.theory_of ctxt
+    val cert = cterm_of thy
+
     val n = length branches
     val scases_idx = map_index I scases
 
     fun inject i ts =
       SumTree.mk_inj T n (i + 1) (foldr1 HOLogic.mk_prod ts)
     val P_of = nth (map (fn (SchemeBranch { P, ... }) => P) branches)
 
-    val thy = Proof_Context.theory_of ctxt
-    val cert = cterm_of thy
-
-    val P_comp = mk_ind_goal thy branches
+    val P_comp = mk_ind_goal ctxt branches
 
     (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)
     val ihyp = Logic.all_const T $ Abs ("z", T,
       Logic.mk_implies
         (HOLogic.mk_Trueprop (

                   |> import
               in
                 sih
                 |> Thm.forall_elim (cert (inject idx rcargs))
                 |> Thm.elim_implies (import ineq) (* Psum rcargs *)
-                |> Conv.fconv_rule sum_prod_conv
-                |> Conv.fconv_rule ind_rulify
+                |> Conv.fconv_rule (sum_prod_conv ctxt)
+                |> Conv.fconv_rule (ind_rulify ctxt)
                 |> (fn th => th COMP ipres) (* P rs *)
                 |> fold_rev (Thm.implies_intr o cprop_of) cGas
                 |> fold_rev Thm.forall_intr cGvs
               end
 

           |> fold_rev (Thm.implies_intr o cprop_of) C_hyps
           |> fold_rev (Thm.forall_intr o cert o Free) ws
 
         val Pxs = cert (HOLogic.mk_Trueprop (P_comp $ x))
           |> Goal.init
-          |> (Simplifier.rewrite_goals_tac (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
-              THEN CONVERSION ind_rulify 1)
+          |> (Simplifier.rewrite_goals_tac ctxt
+                (map meta (branch_hyp :: @{thm split_conv} :: @{thms sum.cases}))
+              THEN CONVERSION (ind_rulify ctxt) 1)
           |> Seq.hd
           |> Thm.elim_implies (Conv.fconv_rule Drule.beta_eta_conversion bstep)
           |> Goal.finish ctxt
           |> Thm.implies_intr (cprop_of branch_hyp)
           |> fold_rev (Thm.forall_intr o cert) fxs

           |> cert
       in
         indthm
         |> Drule.instantiate' [] [SOME inst]
         |> simplify (put_simpset SumTree.sumcase_split_ss ctxt'')
-        |> Conv.fconv_rule ind_rulify
+        |> Conv.fconv_rule (ind_rulify ctxt'')
       end
 
     val res = Conjunction.intr_balanced (map_index project branches)
       |> fold_rev Thm.implies_intr (map cprop_of newgoals @ steps)
       |> Drule.generalize ([], [Rn])