diff -r 020becec359c -r 610794dff23c src/Pure/Isar/proof_display.ML
--- 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 =