src/Pure/General/bytes.scala

--- a/src/Pure/General/bytes.scala	Sat Jun 15 21:59:31 2024 +0200
+++ b/src/Pure/General/bytes.scala	Sat Jun 15 22:43:01 2024 +0200
@@ -384,11 +384,17 @@
       case other: Bytes =>
         if (this.eq(other)) true
         else if (size != other.size) false
-        else if (chunks.isEmpty && size <= 10 * SHA1.digest_length) {
-          Arrays.equals(chunk0, offset.toInt, (offset + size).toInt,
-            other.chunk0, other.offset.toInt, (other.offset + other.size).toInt)
+        else {
+          if (chunks.isEmpty && other.chunks.isEmpty) {
+            Arrays.equals(chunk0, offset.toInt, (offset + size).toInt,
+              other.chunk0, other.offset.toInt, (other.offset + other.size).toInt)
+          }
+          else if (!is_sliced && !other.is_sliced) {
+            (subarray_iterator zip other.subarray_iterator)
+              .forall((a, b) => Arrays.equals(a.array, b.array))
+          }
+          else sha1_digest == other.sha1_digest
         }
-        else sha1_digest == other.sha1_digest
       case _ => false
     }
   }