--- 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