diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/ML/ml_syntax.ML
--- a/src/Pure/ML/ml_syntax.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -147,10 +147,10 @@
 
 val _ =
   ML_system_pp (fn depth => fn _ => fn str =>
-    Pretty.to_polyml (pretty_string' depth str));
+    Pretty.to_ML (pretty_string' depth str));
 
 val _ =
   ML_system_pp (fn depth => fn _ => fn chunks =>
-    Pretty.to_polyml (pretty_string' depth (Long_Name.implode_chunks chunks)));
+    Pretty.to_ML (pretty_string' depth (Long_Name.implode_chunks chunks)));
 
 end;