src/HOL/Tools/Function/induction_schema.ML

     val SchemeBranch { xs, ws, Cs, ... } = nth branches bidx
     val relevant_cases = filter (fn SchemeCase {bidx=bidx', ...} => bidx' = bidx) cases
 
     val allqnames = fold (fn SchemeCase {qs, ...} => fold (insert (op =) o Free) qs) relevant_cases []
     val (Pbool :: xs') = map Free (Variable.variant_frees ctxt allqnames (("P", HOLogic.boolT) :: xs))
-    val Cs' = map (Pattern.rewrite_term (ProofContext.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
+    val Cs' = map (Pattern.rewrite_term (Proof_Context.theory_of ctxt) (filter_out (op aconv) (map Free xs ~~ xs')) []) Cs
 
     fun mk_case (SchemeCase {qs, oqnames, gs, lhs, ...}) =
       HOLogic.mk_Trueprop Pbool
       |> fold_rev (fn x_l => curry Logic.mk_implies (HOLogic.mk_Trueprop(HOLogic.mk_eq x_l)))
            (xs' ~~ lhs)

 
     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 = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val cert = cterm_of thy
 
     val P_comp = mk_ind_goal thy branches
 
     (* Inductive Hypothesis: !!z. (z,x):R ==> P z *)

     val (ctxt', _, cases, concl) = dest_hhf ctxt t
     val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
     val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt'
     val R = Free (Rn, mk_relT ST)
     val x = Free (xn, ST)
-    val cert = cterm_of (ProofContext.theory_of ctxt)
+    val cert = cterm_of (Proof_Context.theory_of ctxt)
 
     val ineqss = mk_ineqs R scheme
       |> map (map (pairself (Thm.assume o cert)))
     val complete =
       map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches)