# HG changeset patch
# User blanchet
# Date 1282048544 -7200
# Node ID 1b460d6a9d583e0f9ce2d94e74102b2903dbae73
# Parent  b8760b6e7c65b8a00f5a3d9366fd4975ba13fc94
improve detection of old Vampire versions

diff -r b8760b6e7c65 -r 1b460d6a9d58 src/HOL/Tools/ATP/atp_systems.ML
--- 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}