# HG changeset patch
# User blanchet
# Date 1314216750 -7200
# Node ID f24b990136ccc615458d869c511623feb03b1cac
# Parent  266dfd7f4e8263eb8a6210491761d0130ca151ce
remove Vampire imconplete proof detection -- the bug it was trying to work around has been fixed in version 1.8, and the check is too sensitive anyway

diff -r 266dfd7f4e82 -r f24b990136cc src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Aug 24 09:23:26 2011 -0700
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Aug 24 22:12:30 2011 +0200
@@ -324,7 +324,6 @@
      [(GaveUp, "UNPROVABLE"),
       (GaveUp, "CANNOT PROVE"),
       (GaveUp, "SZS status GaveUp"),
-      (ProofIncomplete, "predicate_definition_introduction,[]"),
       (TimedOut, "SZS status Timeout"),
       (Unprovable, "Satisfiability detected"),
       (Unprovable, "Termination reason: Satisfiable"),