tuned;

--- a/src/Pure/General/bytes.scala	Fri Jul 05 13:36:49 2024 +0200
+++ b/src/Pure/General/bytes.scala	Fri Jul 05 13:38:35 2024 +0200
@@ -38,11 +38,7 @@
 
   /* main constructors */
 
-  private def reuse_array(bytes: Array[Byte]): Bytes =
-    if (bytes.length <= chunk_size) new Bytes(None, bytes, 0L, bytes.length.toLong)
-    else apply(bytes)
-
-  val empty: Bytes = reuse_array(new Array(0))
+  val empty: Bytes = new Bytes(None, new Array(0), 0L, 0L)
 
   def raw(s: String): Bytes =
     if (s.isEmpty) empty