# HG changeset patch
# User blanchet
# Date 1302773044 -7200
# Node ID 474790ed7b0c99286d1c7b8db920305fb9015be8
# Parent  b3759dcea95e2181f29b2421302549aff2d2ab73
handle Vampire [predicate definition introduction] steps the same way as missing proof, since such steps do not report which axioms were used

diff -r b3759dcea95e -r 474790ed7b0c src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Apr 13 21:38:00 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Apr 14 11:24:04 2011 +0200
@@ -220,6 +220,8 @@
    known_failures =
      [(Unprovable, "UNPROVABLE"),
       (IncompleteUnprovable, "CANNOT PROVE"),
+      (ProofMissing, "[predicate definition introduction]"),
+      (ProofMissing, "predicate_definition_introduction,[]"), (* TSTP *)
       (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
       (Unprovable, "Termination reason: Satisfiable"),