src/Pure/Tools/debugger.ML
changeset 80809 4a64fc4d1cde
parent 78728 72631efa3821
--- a/src/Pure/Tools/debugger.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/Tools/debugger.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -183,7 +183,7 @@
     val space = PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index);
 
     fun print x =
-      Pretty.from_polyml
+      Pretty.from_ML
         (PolyML.NameSpace.Values.printWithType
           (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), SOME space));
     fun print_all () =