src/HOL/Tools/ATP/atp_systems.ML
changeset 52151 de43876e77bf
parent 52097 f353fe3c2b92
child 52754 d9d90d29860e
     1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Sun May 26 12:56:37 2013 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun May 26 14:02:03 2013 +0200
     1.3 @@ -521,11 +521,11 @@
     1.4  (* FIXME: Make "SPASS_NEW_HOME" legacy. *)
     1.5  val spass_config : atp_config =
     1.6    {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
     1.7 -   arguments =
     1.8 -     fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ =>
     1.9 -         "-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^
    1.10 -         file_name
    1.11 -         |> extra_options <> "" ? prefix (extra_options ^ " "),
    1.12 +   arguments = fn _ => fn full_proofs => fn extra_options => fn timeout =>
    1.13 +       fn file_name => fn _ =>
    1.14 +       "-Isabelle=1 " ^ (if full_proofs then "-Splits=0 " else "") ^
    1.15 +       "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name
    1.16 +       |> extra_options <> "" ? prefix (extra_options ^ " "),
    1.17     proof_delims = [("Here is a proof", "Formulae used in the proof")],
    1.18     known_failures =
    1.19       [(OldSPASS, "Unrecognized option Isabelle"),
    1.20 @@ -711,12 +711,12 @@
    1.21  fun remote_config system_name system_versions proof_delims known_failures
    1.22                    prem_role best_slice : atp_config =
    1.23    {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
    1.24 -   arguments =
    1.25 -     fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ =>
    1.26 -         (if command <> "" then "-c " ^ quote command ^ " " else "") ^
    1.27 -         "-s " ^ the_remote_system system_name system_versions ^ " " ^
    1.28 -         "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
    1.29 -         " " ^ file_name,
    1.30 +   arguments = fn _ => fn _ => fn command => fn timeout => fn file_name =>
    1.31 +       fn _ =>
    1.32 +       (if command <> "" then "-c " ^ quote command ^ " " else "") ^
    1.33 +       "-s " ^ the_remote_system system_name system_versions ^ " " ^
    1.34 +       "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
    1.35 +       " " ^ file_name,
    1.36     proof_delims = union (op =) tstp_proof_delims proof_delims,
    1.37     known_failures = known_failures @ known_perl_failures @ known_says_failures,
    1.38     prem_role = prem_role,