fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
authorblanchet
Mon May 30 17:00:38 2011 +0200 (2011-05-30)
changeset 43066e0d4841c5b4a
parent 43065 d1e547e25be2
child 43067 76e1d25c6357
fixed bug in appending special facts introduced in be0e66ccebfa -- if several special facts were added, they overwrote each other
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon May 30 17:00:38 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon May 30 17:00:38 2011 +0200
     1.3 @@ -676,7 +676,7 @@
     1.4        ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
     1.5         (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
     1.6        |> take max_relevant
     1.7 -    fun append_facts ths accepts =
     1.8 +    fun append_to_facts accepts ths =
     1.9        let val add = facts |> filter (member Thm.eq_thm_prop ths o snd) in
    1.10          (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
    1.11                   |> take (max_relevant - length add)) @
    1.12 @@ -685,20 +685,22 @@
    1.13      fun uses_const s t =
    1.14        fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
    1.15                    false
    1.16 -    fun maybe_add_set_const (s, ths) accepts =
    1.17 -      accepts |> (if exists (uses_const s o prop_of o snd) accepts orelse
    1.18 -                     exists (uses_const s) (concl_t :: hyp_ts) then
    1.19 -                    append_facts ths
    1.20 -                  else
    1.21 -                    I)
    1.22 +    fun add_set_const_thms accepts (s, ths) =
    1.23 +      if exists (uses_const s o prop_of o snd) accepts orelse
    1.24 +         exists (uses_const s) (concl_t :: hyp_ts) then
    1.25 +        append ths
    1.26 +      else
    1.27 +        I
    1.28 +    fun append_special_facts accepts =
    1.29 +       [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
    1.30 +          |> fold (add_set_const_thms accepts) set_consts
    1.31 +          |> append_to_facts accepts
    1.32 +
    1.33    in
    1.34      facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)
    1.35            |> iter 0 max_relevant threshold0 goal_const_tab []
    1.36            |> not (null add_ths) ? prepend_facts add_ths
    1.37 -          |> (fn accepts =>
    1.38 -                 accepts |> could_benefit_from_ext is_built_in_const accepts
    1.39 -                            ? append_facts @{thms ext}
    1.40 -                         |> fold maybe_add_set_const set_consts)
    1.41 +          |> append_special_facts
    1.42            |> tap (fn accepts => trace_msg ctxt (fn () =>
    1.43                        "Total relevant: " ^ string_of_int (length accepts)))
    1.44    end