--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 14:21:17 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Feb 20 14:44:00 2013 +0100
@@ -119,7 +119,7 @@
val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix)
fun is_axiom_used_in_proof pred =
- exists (fn ((_, ss), _, _, _, []) => exists pred ss)
+ exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
fun lam_trans_from_atp_proof atp_proof default =
case (is_axiom_used_in_proof is_combinator_def atp_proof,