--- a/src/Pure/General/pretty.ML Tue Sep 10 12:05:37 2024 +0200
+++ b/src/Pure/General/pretty.ML Tue Sep 10 12:22:24 2024 +0200
@@ -247,7 +247,7 @@
let
val {output, escape} = Output.get_mode ();
val {markup, indent} = get_mode ();
- val margin = the_default ML_Pretty.default_margin opt_margin;
+ val margin = ML_Pretty.get_margin opt_margin;
in {output = output, escape = escape, markup = markup, indent = indent, margin = margin} end;
fun markup_output_ops opt_margin : output_ops =
@@ -255,7 +255,7 @@
escape = #escape Output.default_ops,
markup = #markup markup_ops,
indent = #indent markup_ops,
- margin = the_default ML_Pretty.default_margin opt_margin};
+ margin = ML_Pretty.get_margin opt_margin};
fun output_newline (ops: output_ops) = #1 (#output ops "\n");