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