# HG changeset patch
# User blanchet
# Date 1369119778 -7200
# Node ID 17c60b5336fce73cb99aefd2c938be7f94b5faa2
# Parent  018cc7c7e6405ea51e2f792102780ab6212f55d4
prefer compiled version of LEO-II and Satallax if available

diff -r 018cc7c7e640 -r 17c60b5336fc src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue May 21 09:02:58 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue May 21 09:02:58 2013 +0200
@@ -462,7 +462,7 @@
   THF (Monomorphic, TPTP_Explicit, THF_Without_Choice, THF_Without_Defs)
 
 val leo2_config : atp_config =
-  {exec = (["LEO2_HOME"], ["leo"]),
+  {exec = (["LEO2_HOME"], ["leo.opt", "leo"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
        "--foatp e --atp e=\"$E_HOME\"/eprover \
        \--atp epclextract=\"$E_HOME\"/epclextract \
@@ -489,7 +489,7 @@
   THF (Monomorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
 
 val satallax_config : atp_config =
-  {exec = (["SATALLAX_HOME"], ["satallax"]),
+  {exec = (["SATALLAX_HOME"], ["satallax.opt", "satallax"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
        "-p hocore -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name,
    proof_delims =