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) ^ " " ^