# HG changeset patch
# User aspinall
# Date 1171729199 -3600
# Node ID 6c4204df68636ede2a2d465b10bdb77e71a8751d
# Parent  4c96d3370186328aa67f3172d6d77e1cf650ed6d
pretty_full_theory: expose in signature.

diff -r 4c96d3370186 -r 6c4204df6863 src/Pure/Isar/proof_display.ML
--- 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 *)