clean up temporary directory hack
authorblanchet
Thu, 28 Jul 2011 11:49:03 +0200
changeset 43999 04fd92795458
parent 43998 a2aa341bc658
child 44000 ab4d8499815c
clean up temporary directory hack
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