--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Sun Aug 10 14:34:43 2014 +0200
@@ -119,11 +119,13 @@
end
fun thms_in_proof max_thms name_tabs th =
- let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in
- SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names
- (Proofterm.strip_thm (Thm.proof_body_of th)))
- handle TOO_MANY () => NONE
- end
+ (case try Thm.proof_body_of th of
+ NONE => NONE
+ | SOME body =>
+ let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in
+ SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm body))
+ handle TOO_MANY () => NONE
+ end)
fun thms_of_name ctxt name =
let