src/Pure/Isar/proof_context.ML

   val verbose: bool Unsynchronized.ref
   val pretty_ctxt: Proof.context -> Pretty.T list
   val pretty_context: Proof.context -> Pretty.T list
 end;
 
-structure ProofContext: PROOF_CONTEXT =
+structure Proof_Context: PROOF_CONTEXT =
 struct
 
-open ProofContext;
+open Proof_Context;
 
 
 (** inner syntax mode **)
 
 datatype mode =

   in T end;
 
 
 local
 
-val dummies = Config.bool (Config.declare "ProofContext.dummies" (K (Config.Bool false)));
+val dummies = Config.bool (Config.declare "Proof_Context.dummies" (K (Config.Bool false)));
 
 fun check_dummies ctxt t =
   if Config.get ctxt dummies then t
   else Term.no_dummy_patterns t handle TERM _ => error "Illegal dummy pattern(s) in term";
 

     verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts)))
   end;
 
 end;
 
-val show_abbrevs = ProofContext.show_abbrevs;
-
+val show_abbrevs = Proof_Context.show_abbrevs;
+