# HG changeset patch
# User wenzelm
# Date 1025621992 -7200
# Node ID 49f0c90a1bc624b6a1db0e5830a6079bc86ef2f6
# Parent  5e89b6a4ec153576e0cec2a8574eac1b982c4c1d
tuned print_thms_containing;

diff -r 5e89b6a4ec15 -r 49f0c90a1bc6 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jul 02 16:58:57 2002 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jul 02 16:59:52 2002 +0200
@@ -1381,7 +1381,7 @@
 fun print_thms_containing ctxt ss =
   let
     val prt_term = pretty_term ctxt;
-    val prt_fact = pretty_fact ctxt o apsnd (map (#1 o Drule.freeze_thaw));
+    val prt_fact = pretty_fact ctxt;
     fun prt_consts [] = []
       | prt_consts cs = [Pretty.block (Pretty.breaks (Pretty.str "constants" ::
           map (Pretty.quote o prt_term o Syntax.const) cs))];
@@ -1394,7 +1394,7 @@
     val empty_idx = Library.null cs andalso Library.null xs;
 
     val header =
-      if empty_idx then []
+      if empty_idx then [Pretty.block [Pretty.str "All known facts:", Pretty.fbrk]]
       else [Pretty.block (Pretty.breaks (Pretty.str "Facts containing" ::
         separate (Pretty.str "and") (prt_consts cs @ prt_frees xs)) @
           [Pretty.str ":", Pretty.fbrk])]