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