src/HOL/Tools/Function/induction_schema.ML

 
     (* Rule for case splitting along the sum types *)
     val xss = map (fn (SchemeBranch { xs, ... }) => map Free xs) branches
     val pats = map_index (uncurry inject) xss
     val sum_split_rule =
-      Pat_Completeness.prove_completeness thy [x] (P_comp $ x) xss (map single pats)
+      Pat_Completeness.prove_completeness ctxt [x] (P_comp $ x) xss (map single pats)
 
     fun prove_branch (bidx, (SchemeBranch { P, xs, ws, Cs, ... }, (complete_thm, pat))) =
       let
         val fxs = map Free xs
         val branch_hyp = Thm.assume (cert (HOLogic.mk_Trueprop (HOLogic.mk_eq (x, pat))))

               map (Thm.assume o cert o HOLogic.mk_Trueprop o HOLogic.mk_eq) (fxs ~~ lhs)
 
             val cqs = map (cert o Free) qs
             val ags = map (Thm.assume o cert) gs
 
-            val replace_x_ss = HOL_basic_ss addsimps (branch_hyp :: case_hyps)
-            val sih = full_simplify replace_x_ss aihyp
+            val replace_x_simpset =
+              put_simpset HOL_basic_ss ctxt addsimps (branch_hyp :: case_hyps)
+            val sih = full_simplify replace_x_simpset aihyp
 
             fun mk_Prec (idx, Gvs, Gas, rcargs) (ineq, pres) =
               let
                 val cGas = map (Thm.assume o cert) Gas
                 val cGvs = map (cert o Free) Gvs

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