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