--- a/src/Pure/Tools/debugger.ML Thu Mar 17 16:56:44 2016 +0100
+++ b/src/Pure/Tools/debugger.ML Fri Mar 18 16:26:35 2016 +0100
@@ -189,9 +189,8 @@
val space = ML_Debugger.debug_name_space (the_debug_state thread_name index);
fun print x =
- Pretty.from_ML
- (ML_Pretty.from_polyml
- (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space)));
+ Pretty.from_polyml
+ (ML_Name_Space.displayVal (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space));
fun print_all () =
#allVal (ML_Debugger.debug_local_name_space (the_debug_state thread_name index)) ()
|> sort_by #1 |> map (Pretty.item o single o print o #2)