diff -r 1995b421d8ef -r 1222c010bff7 src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Tue Feb 28 17:48:28 2017 +0100
+++ b/src/Pure/General/bytes.scala	Tue Feb 28 17:51:49 2017 +0100
@@ -9,6 +9,7 @@
 
 import java.io.{File => JFile, ByteArrayOutputStream, ByteArrayInputStream,
   OutputStream, InputStream, FileInputStream, FileOutputStream}
+import java.net.URL
 
 import org.tukaani.xz.{XZInputStream, XZOutputStream}
 
@@ -60,6 +61,8 @@
 
   def read(path: Path): Bytes = read(path.file)
 
+  def read(url: URL): Bytes = using(url.openStream)(read_stream(_))
+
 
   /* write */