tmp_name;
authorwenzelm
Fri, 05 Dec 1997 08:01:03 +0100
changeset 4367 2f0c174036dc
parent 4366 4d84cdb0df42
child 4368 1f2dd130fe39
tmp_name;
src/Pure/Thy/thy_read.ML
src/Pure/Thy/use.ML
--- a/src/Pure/Thy/thy_read.ML	Thu Dec 04 14:11:37 1997 +0100
+++ b/src/Pure/Thy/thy_read.ML	Fri Dec 05 08:01:03 1997 +0100
@@ -49,7 +49,7 @@
        
 
 (*Make name of the TextIO.output ML file for a theory *)
-fun out_name tname = "." ^ tname ^ ".thy.ML";
+fun out_name tname = File.tmp_name (tname ^ ".thy.ML");
 
 
 (*Read a file specified by thy_file containing theory tname*)
--- a/src/Pure/Thy/use.ML	Thu Dec 04 14:11:37 1997 +0100
+++ b/src/Pure/Thy/use.ML	Fri Dec 05 08:01:03 1997 +0100
@@ -44,7 +44,7 @@
         if txt = txt_out then use_orig name
         else
           let
-            val tmp_name = File.tmp_name (Path.base_name name);
+            val tmp_name = File.tmp_name ("." ^ Path.base_name name);
             val _ = File.write tmp_name txt_out;
             val rm = OS.FileSys.remove;
           in