diff -r 5cbaf18d0dfb -r 1acf2d76ac23 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sat Apr 05 20:08:00 2014 +0200
+++ b/src/Pure/General/file.scala	Sat Apr 05 22:37:17 2014 +0200
@@ -142,21 +142,5 @@
   }
 
   def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
-
-
-  /* tmp files */
-
-  def tmp_file(prefix: String): JFile =
-  {
-    val file = JFile.createTempFile(prefix, null)
-    file.deleteOnExit
-    file
-  }
-
-  def with_tmp_file[A](prefix: String)(body: JFile => A): A =
-  {
-    val file = tmp_file(prefix)
-    try { body(file) } finally { file.delete }
-  }
 }