diff -r 020becec359c -r 610794dff23c src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Wed Aug 12 21:38:39 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Thu Aug 13 11:05:19 2015 +0200
@@ -176,7 +176,7 @@
       Pretty.from_ML (ML_Name_Space.display_val (x, ML_Options.get_print_depth (), space));
     fun print_all () =
       #allVal (ML_Debugger.debug_name_space (the_debug_state thread_name index)) ()
-      |> sort_wrt #1 |> map (Pretty.item o single o print o #2)
+      |> sort_by #1 |> map (Pretty.item o single o print o #2)
       |> Pretty.chunks |> Pretty.string_of |> writeln_message;
   in Context.setmp_thread_data (SOME context) print_all () end;