pretty_theorems: use proper PureThy.facts_of;

--- a/src/Pure/Isar/proof_display.ML	Wed Apr 16 21:53:03 2008 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed Apr 16 21:53:04 2008 +0200
@@ -52,20 +52,19 @@
 
 (* theorems and theory *)
 
-fun pretty_theorems_diff prev_thms thy =
+fun pretty_theorems_diff prev_facts thy =
   let
     val ctxt = ProofContext.init thy;
-    val (space, thms) = PureThy.theorems_of thy;
-    val diff_thmss = Symtab.fold (fn fact =>
-      if not (Symtab.member Thm.eq_thms prev_thms fact) then cons fact else I) thms [];
-    val thmss = diff_thmss |> map (apfst (NameSpace.extern space)) |> Library.sort_wrt #1;
-  in Pretty.big_list "theorems:" (map (ProofContext.pretty_fact ctxt) thmss) end;
+    val facts = PureThy.facts_of thy;
+    val thmss = Facts.fold_static (fn (name, ths) =>
+      if exists (fn prev => Facts.defined prev name) prev_facts then I
+      else cons (Facts.extern facts name, ths)) facts [];
+  in Pretty.big_list "theorems:" (map (ProofContext.pretty_fact ctxt) (sort_wrt #1 thmss)) end;
 
 fun print_theorems_diff prev_thy thy =
-  Pretty.writeln (pretty_theorems_diff (#2 (PureThy.theorems_of prev_thy)) thy);
+  Pretty.writeln (pretty_theorems_diff [PureThy.facts_of prev_thy] thy);
 
-fun pretty_theorems thy = pretty_theorems_diff Symtab.empty thy;
-
+fun pretty_theorems thy = pretty_theorems_diff (map PureThy.facts_of (Theory.parents_of thy)) thy;
 val print_theorems = Pretty.writeln o pretty_theorems;
 
 fun pretty_full_theory verbose thy =