# HG changeset patch
# User wenzelm
# Date 1142370397 -3600
# Node ID 5a575522fd264eba12f35463d361edad526057e8
# Parent  fdb4658eab268257dc1190f7d1963ae90ef18511
added print_stmts;

diff -r fdb4658eab26 -r 5a575522fd26 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 14 22:06:36 2006 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Mar 14 22:06:37 2006 +0100
@@ -64,6 +64,8 @@
   val print_binds: Toplevel.transition -> Toplevel.transition
   val print_lthms: Toplevel.transition -> Toplevel.transition
   val print_cases: Toplevel.transition -> Toplevel.transition
+  val print_stmts: string list * (thmref * Attrib.src list) list
+    -> Toplevel.transition -> Toplevel.transition
   val print_thms: string list * (thmref * Attrib.src list) list
     -> Toplevel.transition -> Toplevel.transition
   val print_prfs: bool -> string list * (thmref * Attrib.src list) list option
@@ -293,7 +295,12 @@
     ProofContext.print_cases (Proof.context_of (Toplevel.proof_of state)));
 
 
-(* print theorems / types / terms / props *)
+(* print theorems, terms, types etc. *)
+
+fun string_of_stmts state ms args = with_modes ms (fn () =>
+  Proof.get_thmss state args
+  |> map (Element.pretty_statement (Proof.context_of state) PureThy.lemmaK)
+  |> Pretty.chunks2 |> Pretty.string_of);
 
 fun string_of_thms state ms args = with_modes ms (fn () =>
   Pretty.string_of (ProofContext.pretty_thms (Proof.context_of state)
@@ -343,6 +350,7 @@
 fun print_item string_of (x, y) = Toplevel.keep (fn state =>
   writeln (string_of (Toplevel.enter_forward_proof state) x y));
 
+val print_stmts = print_item string_of_stmts;
 val print_thms = print_item string_of_thms;
 fun print_prfs full = print_item (string_of_prfs full);
 val print_prop = print_item string_of_prop;