src/Pure/ML/ml_compiler.ML
changeset 80846 9ed32b8a03a9
parent 80809 4a64fc4d1cde
child 80849 e3a419073736
--- 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;