src/HOL/Tools/ATP/recon_translate_proof.ML
changeset 15658 2edb384bf61f
parent 15642 028059faa963
child 15684 5ec4d21889d6
     1.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Tue Apr 05 16:32:47 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Wed Apr 06 12:01:37 2005 +0200
     1.3 @@ -437,7 +437,7 @@
     1.4                                val thmproofstring = proofstring ( thmstring)
     1.5                              val no_returns =List.filter  not_newline ( thmproofstring)
     1.6                              val thmstr = implode no_returns
     1.7 -                               val outfile = TextIO.openOut("thml_file")
     1.8 +                               val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thml_file")))
     1.9                                 val _ = TextIO.output(outfile, "thmstr is "^thmstr)
    1.10                                 val _ = TextIO.flushOut outfile;
    1.11                                 val _ =  TextIO.closeOut outfile