# HG changeset patch
# User blanchet
# Date 1367569594 -7200
# Node ID af2e0b2c4d7efea20eaaf86f3b4c69595700d072
# Parent  f16bd7d2359c0094e8823a17af4cdc453b2f0c43
pass certain readability-enhancing Vampire options only when an Isar proof is needed

diff -r f16bd7d2359c -r af2e0b2c4d7e src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri May 03 05:25:14 2013 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri May 03 10:26:34 2013 +0200
@@ -539,14 +539,18 @@
 
 val vampire_config : atp_config =
   {exec = (["VAMPIRE_HOME"], ["vampire"]),
-   arguments = fn _ => fn _ => fn sos => fn timeout => fn file_name => fn _ =>
+   arguments = fn _ => fn full_proof => fn sos => fn timeout => fn file_name =>
+       fn _ =>
        "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
        " --proof tptp --output_axiom_names on" ^
        (if is_vampire_at_least_1_8 () then
           (* 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"
+          " --forced_options propositional_to_bdd=off" ^
+          (if full_proof then
+             ":splitting=off:equality_proxy=off:general_splitting=off\
+             \:inequality_splitting=0:naming=0"
+           else
+             "")
         else
           "") ^
        " --thanks \"Andrei and Krystof\" --input_file " ^ file_name