# HG changeset patch
# User blanchet
# Date 1369569723 -7200
# Node ID de43876e77bfe2f8c5ab86ace85b51919c51e375
# Parent  41c885784e04e14ff52ed82cd0e8ec86ed8bdb44
disable SPASS's splitting if Isar proofs are desired, because these are not handled by the proof reconstruction code (and it's not clear how to handle them considering the lack of documentation)

diff -r 41c885784e04 -r de43876e77bf src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Sun May 26 12:56:37 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun May 26 14:02:03 2013 +0200
@@ -521,11 +521,11 @@
 (* FIXME: Make "SPASS_NEW_HOME" legacy. *)
 val spass_config : atp_config =
   {exec = (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
-   arguments =
-     fn _ => fn _ => fn extra_options => fn timeout => fn file_name => fn _ =>
-         "-Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^
-         file_name
-         |> extra_options <> "" ? prefix (extra_options ^ " "),
+   arguments = fn _ => fn full_proofs => fn extra_options => fn timeout =>
+       fn file_name => fn _ =>
+       "-Isabelle=1 " ^ (if full_proofs then "-Splits=0 " else "") ^
+       "-TimeLimit=" ^ string_of_int (to_secs 1 timeout) ^ " " ^ file_name
+       |> extra_options <> "" ? prefix (extra_options ^ " "),
    proof_delims = [("Here is a proof", "Formulae used in the proof")],
    known_failures =
      [(OldSPASS, "Unrecognized option Isabelle"),
@@ -711,12 +711,12 @@
 fun remote_config system_name system_versions proof_delims known_failures
                   prem_role best_slice : atp_config =
   {exec = (["ISABELLE_ATP"], ["scripts/remote_atp"]),
-   arguments =
-     fn _ => fn _ => fn command => fn timeout => fn file_name => fn _ =>
-         (if command <> "" then "-c " ^ quote command ^ " " else "") ^
-         "-s " ^ the_remote_system system_name system_versions ^ " " ^
-         "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
-         " " ^ file_name,
+   arguments = fn _ => fn _ => fn command => fn timeout => fn file_name =>
+       fn _ =>
+       (if command <> "" then "-c " ^ quote command ^ " " else "") ^
+       "-s " ^ the_remote_system system_name system_versions ^ " " ^
+       "-t " ^ string_of_int (Int.min (max_remote_secs, to_secs 1 timeout)) ^
+       " " ^ file_name,
    proof_delims = union (op =) tstp_proof_delims proof_delims,
    known_failures = known_failures @ known_perl_failures @ known_says_failures,
    prem_role = prem_role,