--- a/src/HOL/Tools/ATP/atp_systems.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML Tue May 24 00:01:33 2011 +0200
@@ -385,9 +385,9 @@
" -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
^ " -s " ^ the_system system_name system_versions,
proof_delims = union (op =) tstp_proof_delims proof_delims,
- known_failures =
- known_failures @ known_perl_failures @
+ known_failures = known_failures @ known_perl_failures @
[(Unprovable, "says Satisfiable"),
+ (ProofMissing, "says Theorem"),
(IncompleteUnprovable, "says Unknown"),
(IncompleteUnprovable, "says GaveUp"),
(TimedOut, "says Timeout"),