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;