--- a/src/Pure/pure_setup.ML Tue Oct 20 21:26:45 2009 +0200
+++ b/src/Pure/pure_setup.ML Tue Oct 20 21:37:06 2009 +0200
@@ -28,7 +28,7 @@
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";
@@ -42,10 +42,10 @@
(* 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);