diff -r d637611b41bd -r b3c65c984210 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Sat Sep 04 18:21:58 2021 +0200
+++ b/src/Pure/PIDE/yxml.ML	Sat Sep 04 20:01:43 2021 +0200
@@ -85,7 +85,7 @@
 
 (* output *)
 
-fun string_of_body body = Buffer.empty |> fold (traverse Buffer.add) body |> Buffer.content;
+val string_of_body = Buffer.build_content o fold (traverse Buffer.add);
 val string_of = string_of_body o single;
 
 fun write_body path body =