tuned;
authorwenzelm
Mon, 09 Sep 2024 22:59:41 +0200
changeset 80834 28ed6ac50562
parent 80833 6896736dec38
child 80835 abe1661ad692
tuned;
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 *)