src/Pure/General/bytes.scala

--- a/src/Pure/General/bytes.scala	Wed Nov 28 15:11:21 2018 +0100
+++ b/src/Pure/General/bytes.scala	Wed Nov 28 15:38:18 2018 +0100
@@ -139,6 +139,13 @@
 
   lazy val sha1_digest: SHA1.Digest = SHA1.digest(bytes)
 
+  def array: Array[Byte] =
+  {
+    val a = new Array[Byte](length)
+    System.arraycopy(bytes, offset, a, 0, length)
+    a
+  }
+
   def text: String =
     UTF8.decode_chars(s => s, bytes, offset, offset + length).toString