# HG changeset patch
# User wenzelm
# Date 1730025291 -3600
# Node ID b98595f82a889d27397372537a3ea23437ce344d
# Parent  1f64dce814e76939e0993e6887d77f6cba5aa295
tuned;

diff -r 1f64dce814e7 -r b98595f82a88 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sun Oct 27 11:31:42 2024 +0100
+++ b/src/Pure/General/pretty.ML	Sun Oct 27 11:34:51 2024 +0100
@@ -309,10 +309,10 @@
 
 fun output_tree (ops: output_ops) make_length =
   let
-    fun out (ML_Pretty.PrettyBlock (ind, consistent, context, body)) =
+    fun tree (ML_Pretty.PrettyBlock (ind, consistent, context, body)) =
           let
             val indent = long_nat ind;
-            val body' = map out body;
+            val body' = map tree body;
           in
             Block
              {markup = #markup ops (ML_Pretty.markup_get context),
@@ -322,11 +322,11 @@
               body = body',
               length = if make_length then block_length indent body' else ~1}
           end
-      | out (ML_Pretty.PrettyBreak (wd, ind)) = Break (false, long_nat wd, long_nat ind)
-      | out ML_Pretty.PrettyLineBreak = fbreak
-      | out (ML_Pretty.PrettyString s) = Str (#output ops s ||> force_nat)
-      | out (ML_Pretty.PrettyStringWithWidth (s, n)) = Str (s, long_nat n);
-  in out o to_ML end;
+      | tree (ML_Pretty.PrettyBreak (wd, ind)) = Break (false, long_nat wd, long_nat ind)
+      | tree ML_Pretty.PrettyLineBreak = fbreak
+      | tree (ML_Pretty.PrettyString s) = Str (#output ops s ||> force_nat)
+      | tree (ML_Pretty.PrettyStringWithWidth (s, n)) = Str (s, long_nat n);
+  in tree o to_ML end;
 
 end;