1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Tue Mar 20 18:42:45 2012 +0100
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Tue Mar 20 18:42:45 2012 +0100
     1.3 @@ -117,14 +117,14 @@
     1.4  fun run_some_atp ctxt format problem =
     1.5    let
     1.6      val thy = Proof_Context.theory_of ctxt
     1.7 -    val prob_file = File.tmp_path (Path.explode "prob.tptp")
     1.8 +    val prob_file = File.tmp_path (Path.explode "prob")
     1.9      val atp = case format of DFG _ => spass_newN | _ => eN
    1.10      val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp
    1.11      val ord = effective_term_order ctxt atp
    1.12      val _ = problem |> lines_for_atp_problem format ord (K [])
    1.13                      |> File.write_list prob_file
    1.14      val command =
    1.15 -      File.shell_path (Path.explode (getenv (fst exec) ^ "/" ^ snd exec)) ^
    1.16 +      File.shell_path (Path.explode (getenv (hd (fst exec)) ^ "/" ^ snd exec)) ^
    1.17        " " ^ arguments ctxt false "" (seconds 1.0) (ord, K [], K []) ^ " " ^
    1.18        File.shell_path prob_file
    1.19    in