# HG changeset patch
# User wenzelm
# Date 1152040973 -7200
# Node ID b62836400a33fc277462cf62012b72b01df60d2b
# Parent  f14c03e08e22270e7209aa4ff023383696456080
print_lthms: include unnamed facts from index;
tuned;

diff -r f14c03e08e22 -r b62836400a33 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Jul 04 21:22:52 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Jul 04 21:22:53 2006 +0200
@@ -1100,15 +1100,6 @@
 
 fun setmp_verbose f x = Library.setmp verbose true f x;
 
-fun pretty_items prt name items =
-  let
-    fun prt_itms (name, [x]) = Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt x]
-      | prt_itms (name, xs) = Pretty.big_list (name ^ ":") (map prt xs);
-  in
-    if null items andalso not (! verbose) then []
-    else [Pretty.big_list name (map prt_itms items)]
-  end;
-
 
 (* local syntax *)
 
@@ -1148,7 +1139,15 @@
 (* local theorems *)
 
 fun pretty_lthms ctxt =
-  pretty_items (pretty_thm ctxt) "facts:" (NameSpace.extern_table (#1 (thms_of ctxt)));
+  let
+    val props = FactIndex.props (fact_index_of ctxt);
+    val facts =
+      (if null props then I else cons ("unnamed", props))
+      (NameSpace.extern_table (#1 (thms_of ctxt)));
+  in
+    if null facts andalso not (! verbose) then []
+    else [Pretty.big_list "facts:" (map (pretty_fact ctxt) facts)]
+  end;
 
 val print_lthms = Pretty.writeln o Pretty.chunks o pretty_lthms;