src/HOL/Tools/Function/function_core.ML

   ags: thm list,
   case_hyp : thm}
 
 
 fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) =
-  ClauseContext { ctxt = ProofContext.transfer thy ctxt,
+  ClauseContext { ctxt = Proof_Context.transfer thy ctxt,
     qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp }
 
 
 datatype clause_info = ClauseInfo of
  {no: int,

 fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) =
   let
     val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt
       |>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs
 
-    val thy = ProofContext.theory_of ctxt'
+    val thy = Proof_Context.theory_of ctxt'
 
     fun inst t = subst_bounds (rev qs, t)
     val gs = map inst pre_gs
     val lhs = inst pre_lhs
     val rhs = inst pre_rhs

 fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms =
   let
     val Globals {h, ...} = globals
 
     val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata
-    val cert = Thm.cterm_of (ProofContext.theory_of ctxt)
+    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt)
 
     (* Instantiate the GIntro thm with "f" and import into the clause context. *)
     val lGI = GIntro_thm
       |> Thm.forall_elim (cert f)
       |> fold Thm.forall_elim cqs

 
         val h_assum =
           HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg))
           |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
           |> fold_rev (Logic.all o Free) rcfix
-          |> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] []
+          |> Pattern.rewrite_term (Proof_Context.theory_of ctxt) [(f, h)] []
           |> abstract_over_list (rev qs)
       in
         RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum}
       end
 

 
 
 fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def =
   let
     val Globals {h, domT, ranT, x, ...} = globals
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
 
     (* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *)
     val ihyp = Term.all domT $ Abs ("z", domT,
       Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x),
         HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $

           [] (* no parameters *)
           (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
           [] (* no special monos *)
       ||> Local_Theory.restore_naming lthy
 
-    val cert = cterm_of (ProofContext.theory_of lthy)
+    val cert = cterm_of (Proof_Context.theory_of lthy)
     fun requantify orig_intro thm =
       let
         val (qs, t) = dest_all_all orig_intro
         val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T)
         val vars = Term.add_vars (prop_of thm) [] |> rev

 
 
 (* FIXME: broken by design *)
 fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...},
       qglr = (oqs, _, _, _), ...} = clause
     val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs)
       |> fold_rev (curry Logic.mk_implies) gs
       |> cterm_of thy

       PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
 
     val ((f, (_, f_defthm)), lthy) =
       PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
 
-    val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss
-    val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees
+    val RCss = map (map (inst_RC (Proof_Context.theory_of lthy) fvar f)) RCss
+    val trees = map (Function_Ctx_Tree.inst_tree (Proof_Context.theory_of lthy) fvar f) trees
 
     val ((R, RIntro_thmss, R_elim), lthy) =
       PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
 
     val (_, lthy) =
       Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy
 
-    val newthy = ProofContext.theory_of lthy
+    val newthy = Proof_Context.theory_of lthy
     val clauses = map (transfer_clause_ctx newthy) clauses
 
-    val cert = cterm_of (ProofContext.theory_of lthy)
+    val cert = cterm_of (Proof_Context.theory_of lthy)
 
     val xclauses = PROFILE "xclauses"
       (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
         RCss GIntro_thms) RIntro_thmss