# HG changeset patch
# User wenzelm
# Date 881062806 -3600
# Node ID 472e2df01d3329c835a81527055bb0efbb8e2522
# Parent  4adf0b093275a424c0fcca59a88e04850e1a27dd
File.tmp_name;

diff -r 4adf0b093275 -r 472e2df01d33 src/Pure/Thy/use.ML
--- 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