src/HOL/Tools/Sledgehammer/sledgehammer_util.ML

   in
     snd (app_body map_plain_name body (0, []))
   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
     val lex = Keyword.get_lexicons
     val get = maps (Proof_Context.get_fact ctxt o fst)