print_lthms: include unnamed facts from index;
tuned;

--- 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;