# HG changeset patch
# User blanchet
# Date 1314103459 -7200
# Node ID c76c04d876ef0607ecdc9455c5f1742c5dd32b2b
# Parent  cabd06b69c1813e342ebdab48810d9b486e18e58
kindly ask Vampire to output axiom names

diff -r cabd06b69c18 -r c76c04d876ef src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Aug 23 14:44:19 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Aug 23 14:44:19 2011 +0200
@@ -348,7 +348,6 @@
   Scan.optional ($$ "," |-- parse_annotation
                  --| Scan.option ($$ "," |-- parse_annotations)) []
 
-val vampire_unknown_fact = "unknown"
 val waldmeister_conjecture = "conjecture_1"
 
 val tofof_fact_prefix = "fof_"
@@ -408,9 +407,7 @@
               case deps of
                 ["file", _, s] =>
                 ((num,
-                  if s = vampire_unknown_fact then
-                    NONE
-                  else if s = waldmeister_conjecture then
+                  if s = waldmeister_conjecture then
                     find_formula_in_problem problem (mk_anot phi)
                   else
                     SOME [s |> perhaps (try (unprefix tofof_fact_prefix))]),
diff -r cabd06b69c18 -r c76c04d876ef src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 14:44:19 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Aug 23 14:44:19 2011 +0200
@@ -308,8 +308,9 @@
   {exec = ("VAMPIRE_HOME", "vampire"),
    required_execs = [],
    arguments = fn _ => fn _ => fn sos => fn timeout => fn _ =>
-     "--proof tptp --mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
-     " --thanks \"Andrei and Krystof\" --input_file"
+     "--mode casc -t " ^ string_of_int (to_secs 1 timeout) ^
+     " --proof tptp --output_axiom_names on \
+     \ --thanks \"Andrei and Krystof\" --input_file"
      |> sos = sosN ? prefix "--sos on ",
    proof_delims =
      [("=========== Refutation ==========",