changeset 75615 | 4494cd69f97f |
parent 74231 | b3c65c984210 |
child 75626 | 4879d0021185 |
--- 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 *)