# HG changeset patch
# User blanchet
# Date 1280326414 -7200
# Node ID f6059e2620043c12bf181c7d0b6396e2cab3fa3d
# Parent  4ed1ad92c0ceb5c464f6d13856a0177f8e608d57
adapt to new (?) TPTP output

diff -r 4ed1ad92c0ce -r f6059e262004 src/HOL/Tools/ATP_Manager/SystemOnTPTP
--- a/src/HOL/Tools/ATP_Manager/SystemOnTPTP	Wed Jul 28 15:53:52 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/SystemOnTPTP	Wed Jul 28 16:13:34 2010 +0200
@@ -106,7 +106,7 @@
   exit(-1);
 } elsif (exists($Options{'x'}) &&
   $Response->content =~
-    /%\s*Result\s*:\s*Unsatisfiable.*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
+    /%\s*Result\s*:\s*(Unsatisfiable|Theorem).*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
   $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
 {
   # converted output: extract proof