1.1 --- a/src/HOL/TPTP/atp_export.ML Thu Jul 28 11:43:45 2011 +0200
1.2 +++ b/src/HOL/TPTP/atp_export.ML Thu Jul 28 11:49:03 2011 +0200
1.3 @@ -112,7 +112,7 @@
1.4 fun run_some_atp ctxt problem =
1.5 let
1.6 val thy = Proof_Context.theory_of ctxt
1.7 - val prob_file = Path.explode "/tmp/prob.tptp" (* FIXME File.tmp_path (?) *)
1.8 + val prob_file = File.tmp_path (Path.explode "prob.tptp")
1.9 val {exec, arguments, proof_delims, known_failures, ...} =
1.10 get_atp thy spassN
1.11 val _ = problem |> tptp_lines_for_atp_problem FOF