src/Pure/General/bytes.ML

 
 
 (* IO *)
 
 fun read_block limit =
-  File.input_size (if limit < 0 then chunk_size else Int.min (chunk_size, limit));
+  File_Stream.input_size (if limit < 0 then chunk_size else Int.min (chunk_size, limit));
 
 fun read_stream limit stream =
   let
     fun read bytes =
       (case read_block (limit - length bytes) stream of
         "" => bytes
       | s => read (add s bytes))
   in read empty end;
 
 fun write_stream stream bytes =
-  File.outputs stream (contents bytes);
-
-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;
+  File_Stream.outputs stream (contents bytes);
+
+fun read path = File_Stream.open_input (fn stream => read_stream ~1 stream) path;
+
+fun write path bytes = File_Stream.open_output (fn stream => write_stream stream bytes) path;
 
 
 (* ML pretty printing *)
 
 val _ =