--- 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")],