disable Vampire's BDD optimization, which sometimes yields so huge proofs that this causes problems for reconstruction

--- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 21 11:17:16 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Oct 21 12:44:20 2011 +0200
@@ -344,7 +344,8 @@
    required_execs = [],
    arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
      "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
-     " --proof tptp --output_axiom_names on \
+     " --proof tptp --output_axiom_names on\
+     \ --forced_options propositional_to_bdd=off\
      \ --thanks \"Andrei and Krystof\" --input_file"
      |> sos = sosN ? prefix "--sos on ",
    proof_delims =