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