--- 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;