--- 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))]),
--- 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 ==========",