diff -r fe2c16d9367a -r ed0824ef337e src/Pure/General/bytes.scala
--- a/src/Pure/General/bytes.scala	Mon Dec 03 12:30:37 2018 +0100
+++ b/src/Pure/General/bytes.scala	Mon Dec 03 14:59:42 2018 +0100
@@ -95,11 +95,8 @@
 
   /* write */
 
-  def write(file: JFile, bytes: Bytes)
-  {
-    val stream = new FileOutputStream(file)
-    try { bytes.write_stream(stream) } finally { stream.close }
-  }
+  def write(file: JFile, bytes: Bytes): Unit =
+    using(new FileOutputStream(file))(bytes.write_stream(_))
 
   def write(path: Path, bytes: Bytes): Unit = write(path.file, bytes)
 }