diff -r de97fcc2c624 -r 0eb54e7004eb src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Thu Apr 13 23:08:39 2023 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Thu Apr 13 23:16:18 2023 +0200
@@ -139,8 +139,14 @@
       else take (Int.max (max_len, 0)) body @ ["..."];
   in Pretty.str (quote (implode (map print_symbol body'))) end;
 
+fun pretty_string' depth = pretty_string (FixedInt.toInt (depth * 100));
+
 val _ =
   ML_system_pp (fn depth => fn _ => fn str =>
-    Pretty.to_polyml (pretty_string (FixedInt.toInt (depth * 100)) str));
+    Pretty.to_polyml (pretty_string' depth str));
+
+val _ =
+  ML_system_pp (fn depth => fn _ => fn chunks =>
+    Pretty.to_polyml (pretty_string' depth (Long_Name.implode_chunks chunks)));
 
 end;