# HG changeset patch
# User blanchet
# Date 1411986592 -7200
# Node ID 999adf103930577e762e40a3865acf2b880c7506
# Parent  8438bae06e63ff9420a1bd082250e57c3e5d3731
added option to get cleaner SPASS proofs

diff -r 8438bae06e63 -r 999adf103930 src/HOL/Tools/ATP/atp_systems.ML
--- 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")],