pretty_full_theory: expose in signature.

--- a/src/Pure/Isar/proof_display.ML	Sat Feb 17 17:18:47 2007 +0100
+++ b/src/Pure/Isar/proof_display.ML	Sat Feb 17 17:19:59 2007 +0100
@@ -22,6 +22,7 @@
   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
@@ -72,6 +73,9 @@
 
 val print_theory = print_full_theory false;
 
+fun pretty_full_theory verbose thy =
+    Pretty.chunks (Display.pretty_full_theory verbose thy @ [pretty_theorems thy]);
+
 
 (* refinement rule *)