src/Pure/General/bytes.scala
changeset 55618 995162143ef4
parent 54512 7a92ed889da4
child 60833 d201996f72a8
--- a/src/Pure/General/bytes.scala	Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/General/bytes.scala	Thu Feb 20 14:36:17 2014 +0100
@@ -29,7 +29,7 @@
     if (length == 0) empty
     else {
       val b = new Array[Byte](length)
-      java.lang.System.arraycopy(a, offset, b, 0, length)
+      System.arraycopy(a, offset, b, 0, length)
       new Bytes(b, 0, b.length)
     }
 
@@ -101,8 +101,8 @@
     else if (isEmpty) other
     else {
       val new_bytes = new Array[Byte](length + other.length)
-      java.lang.System.arraycopy(bytes, offset, new_bytes, 0, length)
-      java.lang.System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
+      System.arraycopy(bytes, offset, new_bytes, 0, length)
+      System.arraycopy(other.bytes, other.offset, new_bytes, length, other.length)
       new Bytes(new_bytes, 0, new_bytes.length)
     }