tuned ProofDisplay.pretty_full_theory;

--- a/src/Pure/Isar/isar_cmd.ML	Tue May 08 17:40:18 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue May 08 17:40:20 2007 +0200
@@ -432,7 +432,7 @@
 val print_context = Toplevel.keep Toplevel.print_state_context;
 
 fun print_theory verbose = Toplevel.unknown_theory o
-  Toplevel.keep (ProofDisplay.print_full_theory verbose o Toplevel.theory_of);
+  Toplevel.keep (Pretty.writeln o ProofDisplay.pretty_full_theory verbose o Toplevel.theory_of);
 
 val print_syntax = Toplevel.unknown_context o
   Toplevel.keep (ProofContext.print_syntax o Toplevel.context_of);

--- a/src/Pure/Isar/proof_display.ML	Tue May 08 17:40:18 2007 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue May 08 17:40:20 2007 +0200
@@ -21,14 +21,14 @@
   val pprint_cterm: cterm -> pprint_args -> unit
   val pprint_thm: thm -> pprint_args -> unit
   val print_theorems_diff: theory -> theory -> unit
-  val print_full_theory: bool -> theory -> unit
   val pretty_full_theory: bool -> theory -> Pretty.T
   val string_of_rule: Proof.context -> string -> thm -> string
   val print_results: bool -> Proof.context ->
     ((string * string) * (string * thm list) list) -> unit
   val present_results: Proof.context ->
     ((string * string) * (string * thm list) list) -> unit
-  val pretty_consts: Proof.context -> (string * typ -> bool) -> (string * typ) list -> Pretty.T
+  val pretty_consts: Proof.context ->
+    (string * typ -> bool) -> (string * typ) list -> Pretty.T
 end
 
 structure ProofDisplay: PROOF_DISPLAY =
@@ -47,7 +47,7 @@
 val pprint_term = pprint ProofContext.pretty_term;
 fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
 fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
-val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy true;
+val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
 
 
 (* theorems and theory *)
@@ -68,13 +68,10 @@
 
 val print_theorems = Pretty.writeln o pretty_theorems;
 
-fun print_full_theory verbose thy =
-  Pretty.writeln (Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]));
+fun pretty_full_theory verbose thy =
+  Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
 
-val print_theory = print_full_theory false;
-
-fun pretty_full_theory verbose thy =
-    Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
+val print_theory = Pretty.writeln o pretty_full_theory false;
 
 
 (* refinement rule *)