1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 17 13:10:58 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 17 14:35:44 2010 +0200
     1.3 @@ -183,7 +183,7 @@
     1.4     required_execs = [],
     1.5     arguments = fn _ => fn timeout =>
     1.6       "--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
     1.7 -     " --input_file ",
     1.8 +     " --input_file",
     1.9     proof_delims =
    1.10       [("=========== Refutation ==========",
    1.11         "======= End of refutation ======="),
    1.12 @@ -195,7 +195,7 @@
    1.13        (TimedOut, "SZS status Timeout"),
    1.14        (Unprovable, "Satisfiability detected"),
    1.15        (OutOfResources, "Refutation not found"),
    1.16 -      (OldVampire, "input_file")],
    1.17 +      (OldVampire, "not a valid option")],
    1.18     max_new_relevant_facts_per_iter = 50 (* FIXME *),
    1.19     prefers_theory_relevant = false,
    1.20     explicit_forall = false}