src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

   String.isSubstring ascii_of_lam_fact_prefix s
 
 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,
         is_axiom_used_in_proof is_lam_lifted atp_proof) of
     (false, false) => default