--- a/src/HOL/Tools/ATP/recon_translate_proof.ML Tue Apr 05 16:32:47 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML Wed Apr 06 12:01:37 2005 +0200
@@ -437,7 +437,7 @@
val thmproofstring = proofstring ( thmstring)
val no_returns =List.filter not_newline ( thmproofstring)
val thmstr = implode no_returns
- val outfile = TextIO.openOut("thml_file")
+ val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thml_file")))
val _ = TextIO.output(outfile, "thmstr is "^thmstr)
val _ = TextIO.flushOut outfile;
val _ = TextIO.closeOut outfile