--- a/src/Pure/Isar/proof_display.ML Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/Isar/proof_display.ML Thu Aug 13 11:05:19 2015 +0200
@@ -65,7 +65,7 @@
val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
val facts = Global_Theory.facts_of thy;
val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
- val prts = map #1 (sort_wrt (#1 o #2) (map (`pretty_fact) thmss));
+ val prts = map #1 (sort_by (#1 o #2) (map (`pretty_fact) thmss));
in if null prts then [] else [Pretty.big_list "theorems:" prts] end;
fun pretty_theorems verbose thy =