# HG changeset patch
# User wenzelm
# Date 1725915581 -7200
# Node ID 28ed6ac50562b5df3baad6c2cbcb07b9ec5ec85a
# Parent  6896736dec386c98a6c4b0842770dbd803565d62
tuned;

diff -r 6896736dec38 -r 28ed6ac50562 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Mon Sep 09 22:40:33 2024 +0200
+++ b/src/Pure/General/pretty.ML	Mon Sep 09 22:59:41 2024 +0200
@@ -424,12 +424,12 @@
   in Buffer.build o out o output_tree ops false end;
 
 (*unformatted output*)
-fun unformatted ops prt =
+fun unformatted ops =
   let
     fun out (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold out prts #> Buffer.add en
       | out (Break (_, wd, _)) = output_spaces' ops wd
       | out (Str (s, _)) = Buffer.add s;
-  in Buffer.build (out (output_tree ops false prt)) end;
+  in Buffer.build o out o output_tree ops false end;
 
 
 (* output interfaces *)