diff -r 34906b3db920 -r 4a64fc4d1cde src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/PIDE/xml.ML	Thu Sep 05 17:39:45 2024 +0200
@@ -171,7 +171,7 @@
 
 fun pretty depth tree = Pretty.str (content_depth (Int.max (0, depth)) tree);
 
-val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
+val _ = ML_system_pp (fn depth => fn _ => Pretty.to_ML o pretty (FixedInt.toInt depth));