src/HOL/Tools/ATP/atp_proof.ML

 
   exception UNRECOGNIZED_ATP_PROOF of unit
 
   datatype failure =
     Unprovable |
-    IncompleteUnprovable |
+    GaveUp |
     ProofMissing |
     ProofIncomplete |
     UnsoundProof of bool * string list |
     CantConnect |
     TimedOut |

 
 exception UNRECOGNIZED_ATP_PROOF of unit
 
 datatype failure =
   Unprovable |
-  IncompleteUnprovable |
+  GaveUp |
   ProofMissing |
   ProofIncomplete |
   UnsoundProof of bool * string list |
   CantConnect |
   TimedOut |

   | involving ss =
     "involving " ^ space_implode " " (Try.serial_commas "and" (map quote ss)) ^
     " "
 
 fun string_for_failure Unprovable = "The problem is unprovable."
-  | string_for_failure IncompleteUnprovable = "The prover gave up."
+  | string_for_failure GaveUp = "The prover gave up."
   | string_for_failure ProofMissing =
     "The prover claims the conjecture is a theorem but did not provide a proof."
   | string_for_failure ProofIncomplete =
     "The prover claims the conjecture is a theorem but provided an incomplete \
     \proof."

                                        known_failures output =
   case (extract_tstplike_proof proof_delims output,
         extract_known_failure known_failures output) of
     (_, SOME ProofIncomplete) => ("", SOME ProofIncomplete)
   | ("", SOME failure) =>
-    ("", SOME (if failure = IncompleteUnprovable andalso complete then Unprovable
+    ("", 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)))
   | (tstplike_proof, _) => (tstplike_proof, NONE)