--- a/src/Pure/ML/ml_compiler.ML Wed Sep 04 16:21:52 2024 +0200
+++ b/src/Pure/ML/ml_compiler.ML Thu Sep 05 17:39:45 2024 +0200
@@ -66,7 +66,7 @@
let
val xml =
PolyML.NameSpace.Values.printType (types, depth, SOME name_space)
- |> Pretty.from_polyml |> Pretty.string_of
+ |> Pretty.from_ML |> Pretty.string_of
|> Output.output |> YXML.parse_body;
in cons (pos, fn () => Markup.ML_typing, fn () => YXML.string_of_body xml) end
end;
@@ -215,7 +215,7 @@
fun message {message = msg, hard, location = loc, context = _} =
let
val pos = Exn_Properties.position_of_polyml_location loc;
- val s = Pretty.string_of (Pretty.from_polyml msg);
+ val s = Pretty.string_of (Pretty.from_ML msg);
val catch_all =
#catch_all flags orelse
(case opt_context of
@@ -237,7 +237,7 @@
let
fun display disp x =
if depth > 0 then
- (write (disp x |> Pretty.from_polyml |> Pretty.string_of); write "\n")
+ (write (disp x |> Pretty.from_ML |> Pretty.string_of); write "\n")
else ();
fun apply_fix (a, b) =