--- a/src/Pure/Tools/debugger.ML Thu Mar 03 11:59:03 2016 +0100
+++ b/src/Pure/Tools/debugger.ML Thu Mar 03 14:03:06 2016 +0100
@@ -190,7 +190,8 @@
fun print x =
Pretty.from_ML
- (ML_Name_Space.display_val (x, FixedInt.fromInt (ML_Options.get_print_depth ()), space));
+ (ML_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)