src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 57882 38bf4de248a6
parent 57756 92fe49c7ab3b
parent 57838 c21f2c52f54b
child 58028 e4250d370657
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sun Aug 10 14:31:06 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Sun Aug 10 14:34:43 2014 +0200
     1.3 @@ -119,11 +119,13 @@
     1.4    end
     1.5  
     1.6  fun thms_in_proof max_thms name_tabs th =
     1.7 -  let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in
     1.8 -    SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names
     1.9 -      (Proofterm.strip_thm (Thm.proof_body_of th)))
    1.10 -    handle TOO_MANY () => NONE
    1.11 -  end
    1.12 +  (case try Thm.proof_body_of th of
    1.13 +    NONE => NONE
    1.14 +  | SOME body =>
    1.15 +    let val map_names = (case name_tabs of SOME p => pairself Symtab.lookup p | NONE => `I SOME) in
    1.16 +      SOME (fold_body_thm max_thms (Thm.get_name_hint th) map_names (Proofterm.strip_thm body))
    1.17 +      handle TOO_MANY () => NONE
    1.18 +    end)
    1.19  
    1.20  fun thms_of_name ctxt name =
    1.21    let