# HG changeset patch
# User wenzelm
# Date 1256067426 -7200
# Node ID a707a1f37d29f5cee5933e7913641384ca6b83dd
# Parent  b75c35574e0465969f98482c8103140ade55217b
fixed SML/NJ toplevel pp;
tuned;

diff -r b75c35574e04 -r a707a1f37d29 src/Pure/pure_setup.ML
--- 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);