src/Pure/Isar/code.ML

 
 fun string_of_typ thy =
   Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy));
 
 fun string_of_const thy c =
-  let val ctxt = ProofContext.init_global thy in
+  let val ctxt = Proof_Context.init_global thy in
     case AxClass.inst_of_param thy c of
       SOME (c, tyco) =>
-        ProofContext.extern_const ctxt c ^ " " ^ enclose "[" "]"
-          (ProofContext.extern_type ctxt tyco)
-    | NONE => ProofContext.extern_const ctxt c
+        Proof_Context.extern_const ctxt c ^ " " ^ enclose "[" "]"
+          (Proof_Context.extern_type ctxt tyco)
+    | NONE => Proof_Context.extern_const ctxt c
   end;
 
 
 (* constants *)
 

   end;
 
 fun cert_signature thy = Logic.varifyT_global o Type.cert_typ (build_tsig thy) o Type.no_tvars;
 
 fun read_signature thy = cert_signature thy o Type.strip_sorts
-  o Syntax.parse_typ (ProofContext.init_global thy);
+  o Syntax.parse_typ (Proof_Context.init_global thy);
 
 fun expand_signature thy = Type.cert_typ_mode Type.mode_syntax (Sign.tsig_of thy);
 
 fun lookup_typ thy = Symtab.lookup ((snd o the_signatures o the_exec) thy);
 

       else error ("Type arguments do not satisfy sort constraints of abstype certificate.");
   in (thm, tyco) end;
 
 fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
 
-fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (ProofContext.init_global thy);
+fun meta_rewrite thy = Local_Defs.meta_rewrite_rule (Proof_Context.init_global thy);
 
 fun mk_eqn thy = error_thm (gen_assert_eqn thy false) o
   apfst (meta_rewrite thy);
 
 fun mk_eqn_warning thy = Option.map (fn (thm, _) => (thm, is_linear thm))

 
 (* diagnostic *)
 
 fun print_codesetup thy =
   let
-    val ctxt = ProofContext.init_global thy;
+    val ctxt = Proof_Context.init_global thy;
     val exec = the_exec thy;
     fun pretty_equations const thms =
       (Pretty.block o Pretty.fbreaks) (
         Pretty.str (string_of_const thy const) :: map (Display.pretty_thm ctxt) thms
       );

     val T_cong = nth Ts pos;
     fun mk_prem z = Free (z, T_cong);
     fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
     val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y));
     fun tac { context, prems } = Simplifier.rewrite_goals_tac prems
-      THEN ALLGOALS (ProofContext.fact_tac [Drule.reflexive_thm]);
+      THEN ALLGOALS (Proof_Context.fact_tac [Drule.reflexive_thm]);
   in Skip_Proof.prove_global thy (x :: y :: zs) [prem] concl tac end;
 
 fun add_case thm thy =
   let
     val (case_const, (k, case_pats)) = case_cert thm;