# HG changeset patch # User blanchet # Date 1406283738 -7200 # Node ID d53b1f876afbbe9c4da2d66570b1b7196e965eca # Parent 47336af5d2b26a3e6963a4eda817af8e537c6b2b compile diff -r 47336af5d2b2 -r d53b1f876afb src/HOL/TPTP/atp_theory_export.ML --- a/src/HOL/TPTP/atp_theory_export.ML Fri Jul 25 12:20:48 2014 +0200 +++ b/src/HOL/TPTP/atp_theory_export.ML Fri Jul 25 12:22:18 2014 +0200 @@ -51,12 +51,11 @@ val thy = Proof_Context.theory_of ctxt val prob_file = File.tmp_path (Path.explode "prob") val atp = atp_of_format format - val {exec, arguments, proof_delims, known_failures, ...} = - get_atp thy atp () + val {exec, arguments, proof_delims, known_failures, ...} = get_atp thy atp () val ord = effective_term_order ctxt atp val _ = problem |> lines_of_atp_problem format ord (K []) |> File.write_list prob_file - val exec = exec () + val exec = exec false val path = getenv (List.last (fst exec)) ^ "/" ^ List.last (snd exec) val command = File.shell_path (Path.explode path) ^ " " ^