1.1 --- a/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 25 12:20:48 2014 +0200
     1.2 +++ b/src/HOL/TPTP/atp_theory_export.ML	Fri Jul 25 12:22:18 2014 +0200
     1.3 @@ -51,12 +51,11 @@
     1.4      val thy = Proof_Context.theory_of ctxt
     1.5      val prob_file = File.tmp_path (Path.explode "prob")
     1.6      val atp = atp_of_format format
     1.7 -    val {exec, arguments, proof_delims, known_failures, ...} =
     1.8 -      get_atp thy atp ()
     1.9 +    val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp ()
    1.10      val ord = effective_term_order ctxt atp
    1.11      val _ = problem |> lines_of_atp_problem format ord (K [])
    1.12                      |> File.write_list prob_file
    1.13 -    val exec = exec ()
    1.14 +    val exec = exec false
    1.15      val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec)
    1.16      val command =
    1.17        File.shell_path (Path.explode path) ^ " " ^