src/Pure/pure_setup.ML

 toplevel_pp ["Thm", "cterm"] "ProofDisplay.pp_cterm";
 toplevel_pp ["Thm", "ctyp"] "ProofDisplay.pp_ctyp";
 toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy";
 toplevel_pp ["Context", "theory"] "Context.pretty_thy";
 toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
-toplevel_pp ["Context", "proof"] "ProofDisplay.pp_context";
+toplevel_pp ["Context", "Proof", "context"] "ProofDisplay.pp_context";
 toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
 toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
 toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
 
 if ml_system = "polyml-experimental"

 else ();
 
 
 (* ML toplevel use commands *)
 
-fun use name          = Toplevel.program (fn () => ThyInfo.use name);
-fun use_thys name     = Toplevel.program (fn () => ThyInfo.use_thys name);
-fun use_thy name      = Toplevel.program (fn () => ThyInfo.use_thy name);
-fun time_use name     = Toplevel.program (fn () => ThyInfo.time_use name);
+fun use name = Toplevel.program (fn () => ThyInfo.use name);
+fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name);
+fun use_thy name = Toplevel.program (fn () => ThyInfo.use_thy name);
+fun time_use name = Toplevel.program (fn () => ThyInfo.time_use name);
 fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
 
 
 (* misc *)