diff -r 01b3da984e55 -r 4494cd69f97f src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Fri Jun 24 23:11:59 2022 +0200
+++ b/src/Pure/PIDE/yxml.ML	Fri Jun 24 23:31:28 2022 +0200
@@ -89,8 +89,8 @@
 val string_of = string_of_body o single;
 
 fun write_body path body =
-  path |> File.open_output (fn file =>
-    fold (traverse (fn s => fn () => File.output file s)) body ());
+  path |> File_Stream.open_output (fn file =>
+    fold (traverse (fn s => fn () => File_Stream.output file s)) body ());
 
 
 (* markup elements *)