src/HOL/Tools/ATP/atp_systems.ML
changeset 58478 999adf103930
parent 58084 9f77084444df
child 58495 aefcb244423f
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Sep 29 10:39:39 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Sep 29 12:29:52 2014 +0200
@@ -461,7 +461,7 @@
   {exec = K (["SPASS_NEW_HOME", "SPASS_HOME"], ["SPASS"]),
    arguments = fn _ => fn full_proofs => fn extra_options => fn timeout =>
        fn file_name => fn _ =>
-       "-Isabelle=1 " ^ (if full_proofs then "-Splits=0 " else "") ^
+       "-Isabelle=1 " ^ (if full_proofs then "-CNFRenaming=0 -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")],