# HG changeset patch
# User wenzelm
# Date 1655714725 -7200
# Node ID 65a2482f772d512fb38a96d610b7c04d1a747581
# Parent  5bba3516ddb5fa32d24879825c978ce785821623
remove unused file following 51e696887b81;

diff -r 5bba3516ddb5 -r 65a2482f772d src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Wed Jun 15 16:55:10 2022 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,31 +0,0 @@
-(*  Title:      Pure/General/bytes.ML
-    Author:     Makarius
-
-Byte-vector messages.
-*)
-
-signature BYTES =
-sig
-  val read_line: BinIO.instream -> string option
-  val read_block: BinIO.instream -> int -> string
-end;
-
-structure Bytes: BYTES =
-struct
-
-fun read_line stream =
-  let
-    val result = trim_line o String.implode o rev;
-    fun read cs =
-      (case BinIO.input1 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 read_block stream n =
-  Byte.bytesToString (BinIO.inputN (stream, n));
-
-end;