src/Pure/Isar/proof_display.ML
changeset 28210 c164d1892553
parent 28092 5886e9359aa8
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/Isar/proof_display.ML	Fri Sep 12 10:54:00 2008 +0200
     1.2 +++ b/src/Pure/Isar/proof_display.ML	Fri Sep 12 12:04:16 2008 +0200
     1.3 @@ -46,8 +46,8 @@
     1.4  fun pretty_theorems_diff prev_thys thy =
     1.5    let
     1.6      val pretty_fact = ProofContext.pretty_fact (ProofContext.init thy);
     1.7 -    val thmss = Facts.extern_static (map PureThy.facts_of prev_thys) (PureThy.facts_of thy);
     1.8 -  in Pretty.big_list "theorems:" (map pretty_fact thmss) end;
     1.9 +    val thmss = Facts.dest_static (map PureThy.facts_of prev_thys) (PureThy.facts_of thy);
    1.10 +  in Pretty.big_list "theorems:" (map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss))) end;
    1.11  
    1.12  fun print_theorems_diff prev_thy thy =
    1.13    Pretty.writeln (pretty_theorems_diff [prev_thy] thy);