src/HOL/Tools/SMT/z3_proof_tools.ML
changeset 40806 59d96f777da3
parent 40681 872b08416fb4
child 41123 3bb9be510a9d
     1.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Nov 29 11:39:00 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Mon Nov 29 23:41:09 2010 +0100
     1.3 @@ -73,8 +73,13 @@
     1.4    |> Option.map (fn inst => Thm.instantiate inst thm)
     1.5  
     1.6  fun net_instance' f net ct =
     1.7 -  let fun first_of f xthms ct = get_first (f (maybe_instantiate ct)) xthms 
     1.8 -  in first_of f (Net.match_term net (Thm.term_of ct)) ct end
     1.9 +  let
    1.10 +    val xthms = Net.match_term net (Thm.term_of ct)
    1.11 +    fun first_of f ct = get_first (f (maybe_instantiate ct)) xthms 
    1.12 +    fun first_of' f ct =
    1.13 +      let val thm = Thm.trivial ct
    1.14 +      in get_first (f (try (fn rule => rule COMP thm))) xthms end
    1.15 +  in (case first_of f ct of NONE => first_of' f ct | some_thm => some_thm) end
    1.16  val net_instance = net_instance' I
    1.17  
    1.18