--- a/src/HOL/Tools/ATP/atp_proof.ML Fri Apr 27 12:16:10 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Fri Apr 27 13:18:55 2012 +0200
@@ -390,6 +390,8 @@
| File_Source _ =>
((num, find_formula_in_problem problem phi), "", [])
| Inference_Source (rule, deps) => ((num, []), rule, deps)
+ fun mk_step () =
+ Inference_Step (name, phi, rule, map (rpair []) deps)
in
case role of
"definition" =>
@@ -399,8 +401,8 @@
| AAtom (ATerm ("equal", _)) =>
(* Vampire's equality proxy axiom *)
Inference_Step (name, phi, rule, map (rpair []) deps)
- | _ => raise UNRECOGNIZED_ATP_PROOF ())
- | _ => Inference_Step (name, phi, rule, map (rpair []) deps)
+ | _ => mk_step ())
+ | _ => mk_step ()
end)
(**** PARSING OF SPASS OUTPUT ****)