src/Pure/ML/ml_compiler.ML
changeset 80849 e3a419073736
parent 80846 9ed32b8a03a9
--- a/src/Pure/ML/ml_compiler.ML	Tue Sep 10 20:36:01 2024 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Wed Sep 11 12:11:47 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;
+              |> YXML.parse_body;
           in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
       end;