# HG changeset patch
# User blanchet
# Date 1406898529 -7200
# Node ID c21f2c52f54bf95cf94305e9a926524b12ff7f0a
# Parent  63e3c45b85e11be462911e3eb54808ff5692e33b
careful when calling 'Thm.proof_body_of' -- it can throw exceptions

diff -r 63e3c45b85e1 -r c21f2c52f54b src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- 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