--- 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 *)