File.tmp_name;

--- a/src/Pure/Thy/use.ML	Tue Dec 02 12:39:03 1997 +0100
+++ b/src/Pure/Thy/use.ML	Tue Dec 02 12:40:06 1997 +0100
@@ -44,7 +44,7 @@
         if txt = txt_out then use_orig name
         else
           let
-            val tmp_name = "/tmp/" ^ Path.base_name name;  (* FIXME unique prefix (!?) *)
+            val tmp_name = File.tmp_name (Path.base_name name);
             val _ = File.write tmp_name txt_out;
             val rm = OS.FileSys.remove;
           in