diff -r eaf66384cfe8 -r 0bd51c6aaa8b src/Pure/System/system_channel.ML
--- a/src/Pure/System/system_channel.ML	Mon Dec 10 20:00:02 2018 +0100
+++ b/src/Pure/System/system_channel.ML	Mon Dec 10 20:20:24 2018 +0100
@@ -19,26 +19,11 @@
 
 datatype T = System_Channel of BinIO.instream * BinIO.outstream;
 
-fun input_line (System_Channel (in_stream, _)) =
-  let
-    val result = trim_line o String.implode o rev;
-    fun read cs =
-      (case BinIO.input1 in_stream of
-        NONE => if null cs then NONE else SOME (result cs)
-      | SOME b =>
-          (case Byte.byteToChar b of
-            #"\n" => SOME (result cs)
-          | c => read (c :: cs)));
-  in read [] end;
+fun input_line (System_Channel (stream, _)) = Bytes.read_line stream;
+fun inputN (System_Channel (stream, _)) n = Bytes.read_block stream n;
 
-fun inputN (System_Channel (in_stream, _)) n =
-  Byte.bytesToString (BinIO.inputN (in_stream, n));
-
-fun output (System_Channel (_, out_stream)) s =
-  File.output out_stream s;
-
-fun flush (System_Channel (_, out_stream)) =
-  BinIO.flushOut out_stream;
+fun output (System_Channel (_, stream)) s = File.output stream s;
+fun flush (System_Channel (_, stream)) = BinIO.flushOut stream;
 
 fun rendezvous name =
   let