added print_theory that prints stored thms;

--- a/src/Pure/Thy/thy_read.ML	Fri Dec 09 16:44:31 1994 +0100
+++ b/src/Pure/Thy/thy_read.ML	Mon Dec 12 10:26:05 1994 +0100
@@ -47,6 +47,7 @@
                  -> unit
   val get_thm: theory -> string -> thm
   val thms_of: theory -> (string * thm) list
+  val print_theory: theory -> unit
 end;
 
 
@@ -529,4 +530,18 @@
 val thms_of = Symtab.dest o thmtab;
 
 
+(* print theory *)
+
+fun print_thms thy =
+  let
+    val thms = thms_of thy;
+    fun prt_thm (s, th) = Pretty.block [Pretty.str (s ^ ":"), Pretty.brk 1,
+      Pretty.quote (pretty_thm th)];
+  in
+    Pretty.writeln (Pretty.big_list "stored theorems:" (map prt_thm thms))
+  end;
+
+fun print_theory thy = (Drule.print_theory thy; print_thms thy);
+
+
 end;