# HG changeset patch
# User blanchet
# Date 1361367840 -3600
# Node ID 3278cd5de3b113dff1a8b256ec2ebb417a7db655
# Parent  f176855a1ee2ba095d2988f7f8acaaaba40681c7
added case taken out by mistake

diff -r f176855a1ee2 -r 3278cd5de3b1 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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,