--- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 17 13:10:58 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 17 14:35:44 2010 +0200
@@ -183,7 +183,7 @@
required_execs = [],
arguments = fn _ => fn timeout =>
"--mode casc -t " ^ string_of_int (to_generous_secs timeout) ^
- " --input_file ",
+ " --input_file",
proof_delims =
[("=========== Refutation ==========",
"======= End of refutation ======="),
@@ -195,7 +195,7 @@
(TimedOut, "SZS status Timeout"),
(Unprovable, "Satisfiability detected"),
(OutOfResources, "Refutation not found"),
- (OldVampire, "input_file")],
+ (OldVampire, "not a valid option")],
max_new_relevant_facts_per_iter = 50 (* FIXME *),
prefers_theory_relevant = false,
explicit_forall = false}