# HG changeset patch
# User blanchet
# Date 1361353501 -3600
# Node ID 1ff19dfd3111af43282d04e23593da3388293310
# Parent  d995fae02981067027faa0488970953687a1e4e0
turn off more evil Vampire options to facilitate Isar proof generation

diff -r d995fae02981 -r 1ff19dfd3111 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Feb 20 09:58:28 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Feb 20 10:45:01 2013 +0100
@@ -543,7 +543,10 @@
        "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
        " --proof tptp --output_axiom_names on" ^
        (if is_vampire_at_least_1_8 () then
-          " --forced_options propositional_to_bdd=off"
+          (* Cf. p. 20 of http://www.complang.tuwien.ac.at/lkovacs/Cade23_Tutorial_Slides/Session2_Slides.pdf *)
+          " --forced_options propositional_to_bdd=off:splitting=off:\
+          \equality_proxy=off:general_splitting=off:inequality_splitting=0:\
+          \naming=0"
         else
           "") ^
        " --thanks \"Andrei and Krystof\" --input_file " ^ file_name