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