diff -r da20e00050ab -r 9ed32b8a03a9 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Tue Sep 10 16:06:38 2024 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Tue Sep 10 19:57:45 2024 +0200
@@ -67,7 +67,7 @@
             val xml =
               PolyML.NameSpace.Values.printType (types, depth, SOME name_space)
               |> Pretty.from_ML |> Pretty.string_of
-              |> Output.output |> YXML.parse_body;
+              |> Output.output_ |> YXML.parse_body;
           in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
       end;