author | blanchet |
Thu, 28 Jul 2011 11:49:03 +0200 | |
changeset 43999 | 04fd92795458 |
parent 43998 | a2aa341bc658 |
child 44000 | ab4d8499815c |
--- 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