# HG changeset patch
# User blanchet
# Date 1307449055 -7200
# Node ID 01b6391a763feb7a51548a0ef935ff224388dd6e
# Parent  cef69d31bfa459439a0694505ffa2c3e1b05c397
fixed missing proof handling

diff -r cef69d31bfa4 -r 01b6391a763f src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Jun 07 14:17:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Jun 07 14:17:35 2011 +0200
@@ -199,12 +199,11 @@
   case (extract_tstplike_proof proof_delims output,
         extract_known_failure known_failures output) of
     (_, SOME ProofIncomplete) => ("", SOME ProofIncomplete)
+  | ("", SOME ProofMissing) => ("", NONE)
   | ("", SOME failure) =>
     ("", SOME (if failure = GaveUp andalso complete then Unprovable
                else failure))
-  | ("", NONE) =>
-    ("", SOME (if res_code = 0 andalso output = "" then ProofMissing
-               else UnknownError (short_output verbose output)))
+  | ("", NONE) => ("", SOME (UnknownError (short_output verbose output)))
   | (tstplike_proof, _) => (tstplike_proof, NONE)
 
 type step_name = string * string option