src/HOL/Tools/inductive.ML

 val get_inductives = InductiveData.get o Context.Proof;
 
 fun print_inductives ctxt =
   let
     val (tab, monos) = get_inductives ctxt;
-    val space = Consts.space_of (ProofContext.consts_of ctxt);
+    val space = Consts.space_of (Proof_Context.consts_of ctxt);
   in
     [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, tab))),
      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
     |> Pretty.chunks |> Pretty.writeln
   end;

     val params' = Term.variant_frees rule (Logic.strip_params rule);
     val frees = rev (map Free params');
     val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
     val prems = map (curry subst_bounds frees) (Logic.strip_assums_hyp rule);
     val rule' = Logic.list_implies (prems, concl);
-    val aprems = map (atomize_term (ProofContext.theory_of ctxt)) prems;
+    val aprems = map (atomize_term (Proof_Context.theory_of ctxt)) prems;
     val arule = list_all_free (params', Logic.list_implies (aprems, concl));
 
     fun check_ind err t = case dest_predicate cs params t of
         NONE => err (bad_app ^
           commas (map (Syntax.string_of_term ctxt) params))

         rtac (unfold RS iffD2) 1,
         EVERY1 (select_disj (length intr_ts) (i + 1)),
         (*Not ares_tac, since refl must be tried before any equality assumptions;
           backtracking may occur if the premises have extra variables!*)
         DEPTH_SOLVE_1 (resolve_tac rules 1 APPEND assume_tac 1)])
-       |> singleton (ProofContext.export ctxt ctxt')) intr_ts
+       |> singleton (Proof_Context.export ctxt ctxt')) intr_ts
 
   in (intrs, unfold) end;
 
 
 (* prove elimination rules *)

              dtac (unfold RS iffD1) 1,
              REPEAT (FIRSTGOAL (eresolve_tac rules1)),
              REPEAT (FIRSTGOAL (eresolve_tac rules2)),
              EVERY (map (fn prem =>
                DEPTH_SOLVE_1 (ares_tac [rewrite_rule rec_preds_defs prem, conjI] 1)) (tl prems))])
-          |> singleton (ProofContext.export ctxt'' ctxt'''),
+          |> singleton (Proof_Context.export ctxt'' ctxt'''),
          map #2 c_intrs, length Ts)
       end
 
    in map prove_elim cs end;
 

             let val (c_intrs', last_c_intr) = split_last c_intrs in
               EVERY (map (fn ci => etac @{thm disjE} 1 THEN prove_intr2 ci) c_intrs')
               THEN prove_intr2 last_c_intr
             end))
         |> rulify
-        |> singleton (ProofContext.export ctxt' ctxt'')
+        |> singleton (Proof_Context.export ctxt' ctxt'')
       end;  
   in
     map2 prove_eq cs elims
   end;
   

 
 in
 
 fun mk_cases ctxt prop =
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     val ss = simpset_of ctxt;
 
     fun err msg =
       error (Pretty.string_of (Pretty.block
         [Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt prop]));

 
 (* inductive_cases *)
 
 fun gen_inductive_cases prep_att prep_prop args lthy =
   let
-    val thy = ProofContext.theory_of lthy;
+    val thy = Proof_Context.theory_of lthy;
     val facts = args |> Par_List.map (fn ((a, atts), props) =>
       ((a, map (prep_att thy) atts),
         Par_List.map (Thm.no_attributes o single o mk_cases lthy o prep_prop lthy) props));
   in lthy |> Local_Theory.notes facts |>> map snd end;
 

       (fn (raw_props, fixes) => fn ctxt =>
         let
           val (_, ctxt') = Variable.add_fixes fixes ctxt;
           val props = Syntax.read_props ctxt' raw_props;
           val ctxt'' = fold Variable.declare_term props ctxt';
-          val rules = ProofContext.export ctxt'' ctxt (map (mk_cases ctxt'') props)
+          val rules = Proof_Context.export ctxt'' ctxt (map (mk_cases ctxt'') props)
         in Method.erule 0 rules end))
     "dynamic case analysis on predicates";
 
 (* derivation of simplified equation *)
 
 fun mk_simp_eq ctxt prop =
   let
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     val ctxt' = Variable.auto_fixes prop ctxt
     val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of
     val substs = Item_Net.retrieve (Equation_Data.get (Context.Proof ctxt)) (HOLogic.dest_Trueprop prop) 
       |> map_filter
         (fn eq => SOME (Pattern.match thy (lhs_of eq, HOLogic.dest_Trueprop prop)

 
 (* inductive simps *)
 
 fun gen_inductive_simps prep_att prep_prop args lthy =
   let
-    val thy = ProofContext.theory_of lthy;
+    val thy = Proof_Context.theory_of lthy;
     val facts = args |> map (fn ((a, atts), props) =>
       ((a, map (prep_att thy) atts),
         map (Thm.no_attributes o single o mk_simp_eq lthy o prep_prop lthy) props));
   in lthy |> Local_Theory.notes facts |>> map snd end;
 

 
 fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono
     fp_def rec_preds_defs ctxt ctxt''' =
   let
     val _ = clean_message quiet_mode "  Proving the induction rule ...";
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
 
     (* predicates for induction rule *)
 
     val (pnames, ctxt') = Variable.variant_fixes (mk_names "P" (length cs)) ctxt;
     val preds = map2 (curry Free) pnames

             REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
             atac 1,
             rewrite_goals_tac simp_thms',
             atac 1])])
 
-  in singleton (ProofContext.export ctxt'' ctxt''') (induct RS lemma) end;
+  in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
 
 
 
 (** specification of (co)inductive predicates **)
 

          ((Binding.empty, [Attrib.internal (K Nitpick_Unfolds.add)]),
          fold_rev lambda params
            (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
       ||> Local_Theory.restore_naming lthy;
     val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
-      (cterm_of (ProofContext.theory_of lthy') (list_comb (rec_const, params)));
+      (cterm_of (Proof_Context.theory_of lthy') (list_comb (rec_const, params)));
     val specs =
       if length cs < 2 then []
       else
         map_index (fn (i, (name_mx, c)) =>
           let

 
     val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
     val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy''';
     val (_, lthy'''') =
       Local_Theory.note (apfst Binding.conceal Attrib.empty_binding,
-        ProofContext.export lthy''' lthy'' [mono]) lthy'';
+        Proof_Context.export lthy''' lthy'' [mono]) lthy'';
 
   in (lthy'''', lthy''', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
     list_comb (rec_const, params), preds, argTs, bs, xs)
   end;
 

         prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names)
           unfold rec_preds_defs lthy2 lthy1;
     val raw_induct = zero_var_indexes
       (if no_ind then Drule.asm_rl
        else if coind then
-         singleton (ProofContext.export lthy2 lthy1)
+         singleton (Proof_Context.export lthy2 lthy1)
            (rotate_prems ~1 (Object_Logic.rulify
              (fold_rule rec_preds_defs
                (rewrite_rule simp_thms'''
                 (mono RS (fp_def RS @{thm def_coinduct}))))))
        else

 
 fun gen_add_inductive_i mk_def
     (flags as {quiet_mode, verbose, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono})
     cnames_syn pnames spec monos lthy =
   let
-    val thy = ProofContext.theory_of lthy;
+    val thy = Proof_Context.theory_of lthy;
     val _ = Theory.requires thy "Inductive" (coind_prefix coind ^ "inductive definitions");
 
 
     (* abbrevs *)
 

     val ps = map Free pnames;
 
     val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn');
     val _ = map (fn abbr => Local_Defs.fixed_abbrev abbr ctxt2) abbrevs;
     val ctxt3 = ctxt2 |> fold (snd oo Local_Defs.fixed_abbrev) abbrevs;
-    val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
+    val expand = Assumption.export_term ctxt3 lthy #> Proof_Context.cert_term lthy;
 
     fun close_rule r = list_all_free (rev (fold_aterms
       (fn t as Free (v as (s, _)) =>
           if Variable.is_fixed ctxt1 s orelse
             member (op =) ps t then I else insert (op =) v

   end;
 
 fun gen_add_inductive mk_def verbose coind cnames_syn pnames_syn intro_srcs raw_monos int lthy =
   let
     val ((vars, intrs), _) = lthy
-      |> ProofContext.set_mode ProofContext.mode_abbrev
+      |> Proof_Context.set_mode Proof_Context.mode_abbrev
       |> Specification.read_spec (cnames_syn @ pnames_syn) intro_srcs;
     val (cs, ps) = chop (length cnames_syn) vars;
     val monos = Attrib.eval_thms lthy raw_monos;
     val flags = {quiet_mode = false, verbose = verbose, alt_name = Binding.empty,
       coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int};

     val ctxt' = thy
       |> Named_Target.theory_init
       |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
       |> Local_Theory.exit;
     val info = #2 (the_inductive ctxt' name);
-  in (info, ProofContext.theory_of ctxt') end;
+  in (info, Proof_Context.theory_of ctxt') end;
 
 
 (* read off arities of inductive predicates from raw induction rule *)
 fun arities_of induct =
   map (fn (_ $ t $ u) =>