# HG changeset patch
# User blanchet
# Date 1338971705 -7200
# Node ID e6cffd467ff5cf776ef07036be335ba2d291d152
# Parent  a4148c95134d99d6f48bb0eac793892bacf79646
robust LEO-II setup that doesn't rely on ".leoatprc"

diff -r a4148c95134d -r e6cffd467ff5 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Jun 06 10:35:05 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Jun 06 10:35:05 2012 +0200
@@ -337,7 +337,10 @@
    required_vars = [],
    arguments =
      fn _ => fn _ => fn _ => fn timeout => fn _ =>
-        "--proofoutput 1 --timeout " ^ string_of_int (to_secs 1 timeout),
+        "--foatp e --atp e=\"$E_HOME\"/eprover \
+        \--atp epclextract=\"$E_HOME\"/epclextract \
+        \--proofoutput 1 --timeout " ^
+        string_of_int (to_secs 1 timeout),
    proof_delims = tstp_proof_delims,
    known_failures =
      [(TimedOut, "CPU time limit exceeded, terminating"),