Facts.dest/export_static: content difference;
authorwenzelm
Thu Jun 12 16:41:58 2008 +0200 (2008-06-12)
changeset 271763735b80d06fc
parent 27175 620295a57106
child 27177 adefd3454174
Facts.dest/export_static: content difference;
tuned;
src/Pure/Isar/proof_display.ML
     1.1 --- a/src/Pure/Isar/proof_display.ML	Thu Jun 12 16:41:57 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Thu Jun 12 16:41:58 2008 +0200
     1.3 @@ -52,19 +52,16 @@
     1.4  
     1.5  (* theorems and theory *)
     1.6  
     1.7 -fun pretty_theorems_diff prev_facts thy =
     1.8 +fun pretty_theorems_diff prev_thys thy =
     1.9    let
    1.10 -    val ctxt = ProofContext.init thy;
    1.11 -    val facts = PureThy.facts_of thy;
    1.12 -    val thmss = Facts.fold_static (fn (name, ths) =>
    1.13 -      if exists (fn prev => Facts.defined prev name) prev_facts then I
    1.14 -      else cons (Facts.extern facts name, ths)) facts [];
    1.15 -  in Pretty.big_list "theorems:" (map (ProofContext.pretty_fact ctxt) (sort_wrt #1 thmss)) end;
    1.16 +    val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
    1.17 +    val thmss = Facts.extern_static (map PureThy.facts_of prev_thys) (PureThy.facts_of thy);
    1.18 +  in Pretty.big_list "theorems:" (map pretty_fact thmss) end;
    1.19  
    1.20  fun print_theorems_diff prev_thy thy =
    1.21 -  Pretty.writeln (pretty_theorems_diff [PureThy.facts_of prev_thy] thy);
    1.22 +  Pretty.writeln (pretty_theorems_diff [prev_thy] thy);
    1.23  
    1.24 -fun pretty_theorems thy = pretty_theorems_diff (map PureThy.facts_of (Theory.parents_of thy)) thy;
    1.25 +fun pretty_theorems thy = pretty_theorems_diff (Theory.parents_of thy) thy;
    1.26  val print_theorems = Pretty.writeln o pretty_theorems;
    1.27  
    1.28  fun pretty_full_theory verbose thy =