src/HOL/Tools/ATP/recon_translate_proof.ML

                              let (* val _ = reset show_sorts*)
                               val thmstring = Meson.concat_with_and (map string_of_thm (map snd thml))
                               val thmproofstring = proofstring ( thmstring)
                             val no_returns =List.filter  not_newline ( thmproofstring)
                             val thmstr = implode no_returns
-                               val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thml_file")))
+                               val outfile = TextIO.openOut(File.platform_path(File.tmp_path (Path.basic "thml_file")))
                                val _ = TextIO.output(outfile, "thmstr is "^thmstr)
                                val _ = TextIO.flushOut outfile;
                                val _ =  TextIO.closeOut outfile
                                  (*val _ = set show_sorts*)
                              in