src/HOL/Tools/ATP/atp_proof.ML

 signature ATP_PROOF =
 sig
   type 'a fo_term = 'a ATP_Problem.fo_term
   type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
   type 'a problem = 'a ATP_Problem.problem
+
+  exception UNRECOGNIZED_ATP_PROOF of unit
 
   datatype failure =
     Unprovable |
     IncompleteUnprovable |
     ProofMissing |

 
 structure ATP_Proof : ATP_PROOF =
 struct
 
 open ATP_Problem
+
+exception UNRECOGNIZED_ATP_PROOF of unit
 
 datatype failure =
   Unprovable |
   IncompleteUnprovable |
   ProofMissing |

 fun parse_line problem = parse_tstp_line problem || parse_spass_line
 fun parse_proof problem s =
   s |> strip_spaces_except_between_ident_chars
     |> raw_explode
     |> Scan.finite Symbol.stopper
-           (Scan.error (!! (fn _ => raise Fail "unrecognized ATP output")
+           (Scan.error (!! (fn _ => raise UNRECOGNIZED_ATP_PROOF ())
                            (Scan.repeat1 (parse_line problem))))
     |> fst
 
 fun clean_up_dependency seen dep = find_first (curry is_same_step dep) seen
 fun clean_up_dependencies _ [] = []