# HG changeset patch
# User wenzelm
# Date 938029777 -7200
# Node ID 18070ae7a84c3a518dc7a16a72fed3808a423e09
# Parent  536499cf71afb811f0d0c0274a60c345c21098d7
thms_containing: single writeln;

diff -r 536499cf71af -r 18070ae7a84c src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Wed Sep 22 21:45:35 1999 +0200
+++ b/src/Pure/Interface/proof_general.ML	Wed Sep 22 21:49:37 1999 +0200
@@ -160,11 +160,14 @@
 
 (* some top-level commands for ProofGeneral/isa *)
 
-fun print_thm (a, th) =
-  Pretty.writeln (Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
-    Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))]);
+fun prt_thm (a, th) =
+  Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
+    Display.pretty_thm_no_quote (#1 (Drule.freeze_thaw th))];
 
-val thms_containing = seq print_thm o ThmDatabase.thms_containing;
+fun thms_containing cs =
+  Pretty.blk (0, Pretty.fbreaks (map prt_thm (ThmDatabase.thms_containing cs)))
+  |> Pretty.writeln;
+
 
 val help = writeln o Session.welcome;
 val show_context = Context.the_context;