careful when calling 'Thm.proof_body_of' -- it can throw exceptions

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Aug 01 20:43:23 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Aug 01 15:08:49 2014 +0200
@@ -116,11 +116,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