--- 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 =