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