--- 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;