Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned print_thms_containing;
authorwenzelm
Tue, 02 Jul 2002 16:59:52 +0200
changeset 13282 49f0c90a1bc6
parent 13281 5e89b6a4ec15
child 13283 1051aa66cbf3
tuned print_thms_containing;
src/Pure/Isar/proof_context.ML file | annotate | diff | comparison | revisions 
--- 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])]
isabelle