diff -r 95449e4b4bf6 -r bb8468ae414e src/Tools/cache_io.ML
--- a/src/Tools/cache_io.ML	Mon Dec 20 13:36:25 2010 +0100
+++ b/src/Tools/cache_io.ML	Mon Dec 20 14:44:00 2010 +0100
@@ -7,8 +7,6 @@
 signature CACHE_IO =
 sig
   (*IO wrapper*)
-  val with_tmp_file: string -> (Path.T -> 'a) -> 'a
-  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
   type result = {
     output: string list,
     redirected_output: string list,
@@ -34,21 +32,6 @@
 
 val cache_io_prefix = "cache-io-"
 
-fun with_tmp_file name f =
-  let
-    val path = File.tmp_path (Path.explode (name ^ serial_string ()))
-    val x = Exn.capture f path
-    val _ = try File.rm path
-  in Exn.release x end
-
-fun with_tmp_dir name f =
-  let
-    val path = File.tmp_path (Path.explode (name ^ serial_string ()))
-    val _ = Isabelle_System.mkdirs path
-    val x = Exn.capture f path
-    val _ = try Isabelle_System.rm_tree path
-  in Exn.release x end
-
 type result = {
   output: string list,
   redirected_output: string list,
@@ -62,8 +45,9 @@
   in {output=split_lines out2, redirected_output=out1, return_code=rc} end
 
 fun run make_cmd str =
-  with_tmp_file cache_io_prefix (fn in_path =>
-  with_tmp_file cache_io_prefix (raw_run make_cmd str in_path))
+  Isabelle_System.with_tmp_file cache_io_prefix (fn in_path =>
+    Isabelle_System.with_tmp_file cache_io_prefix (fn out_path =>
+      raw_run make_cmd str in_path out_path))
 
 
 (* cache *)