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