src/Pure/General/bytes.ML

--- a/src/Pure/General/bytes.ML	Tue Jun 21 14:08:02 2022 +0200
+++ b/src/Pure/General/bytes.ML	Tue Jun 21 14:22:34 2022 +0200
@@ -70,13 +70,10 @@
 
 val buffer = build o fold add o Buffer.contents;
 
-fun read_chunk stream =
-  Byte.bytesToString (BinIO.inputN (stream, chunk_size));
-
 val read = File.open_input (fn stream =>
   let
     fun read_bytes bytes =
-      (case read_chunk stream of
+      (case File.input_size chunk_size stream of
         "" => bytes
       | s => read_bytes (add s bytes))
   in read_bytes empty end);