# HG changeset patch
# User wenzelm
# Date 1656012323 -7200
# Node ID 7a0d4c126f79fa9b5619ab13e32085271fc60ed3
# Parent  e6e0a95f87f3072eac5cc879ee5a2d7387d4871a
proper execution of Bytes.write;
tuned;

diff -r e6e0a95f87f3 -r 7a0d4c126f79 src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Wed Jun 22 17:07:00 2022 +0200
+++ b/src/Pure/General/bytes.ML	Thu Jun 23 21:25:23 2022 +0200
@@ -196,10 +196,12 @@
       | s => read (add s bytes))
   in read empty end;
 
-fun write_stream stream = File.outputs stream o contents;
+fun write_stream stream bytes =
+  File.outputs stream (contents bytes);
 
-val read = File.open_input (read_stream ~1);
-val write = File.open_output write_stream;
+fun read path = File.open_input (fn stream => read_stream ~1 stream) path;
+
+fun write path bytes = File.open_output (fn stream => write_stream stream bytes) path;
 
 
 (* ML pretty printing *)