src/Pure/PIDE/yxml.ML

 fun string_of_body body = Buffer.empty |> fold buffer body |> Buffer.content;
 val string_of = string_of_body o single;
 
 fun write_body path body =
   path |> File.open_output (fn file =>
-    fold (traverse (fn s => fn () => BinIO.output (file, Byte.stringToBytes s))) body ());
+    fold (traverse (fn s => fn () => File.output file s)) body ());
 
 
 (* markup elements *)
 
 val Z = chr 0;