diff -r df85df6315af -r e3a419073736 src/Pure/ML/ml_compiler.ML --- 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;