# HG changeset patch
# User blanchet
# Date 1311846543 -7200
# Node ID 04fd92795458f1f8101a83f897e9991f6c5e2564
# Parent  a2aa341bc6581da87ceb0dc1ccd1fe1aaf0d7ce5
clean up temporary directory hack

diff -r a2aa341bc658 -r 04fd92795458 src/HOL/TPTP/atp_export.ML
--- a/src/HOL/TPTP/atp_export.ML	Thu Jul 28 11:43:45 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML	Thu Jul 28 11:49:03 2011 +0200
@@ -112,7 +112,7 @@
 fun run_some_atp ctxt problem =
   let
     val thy = Proof_Context.theory_of ctxt
-    val prob_file = Path.explode "/tmp/prob.tptp"  (* FIXME File.tmp_path (?) *)
+    val prob_file = File.tmp_path (Path.explode "prob.tptp")
     val {exec, arguments, proof_delims, known_failures, ...} =
       get_atp thy spassN
     val _ = problem |> tptp_lines_for_atp_problem FOF