# HG changeset patch # User blanchet # Date 1305637896 -7200 # Node ID be0e66ccebfa826c306b8ff63679cf1636639b15 # Parent b04436548927c1321d606c3328ecf002df9bd1aa append special boring facts rather than prepend them, to avoid confusing E's weighting mechanism diff -r b04436548927 -r be0e66ccebfa src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon May 16 23:41:10 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue May 17 15:11:36 2011 +0200 @@ -672,26 +672,32 @@ |> map string_for_hyper_pconst)); relevant [] [] hopeful end - fun add_facts ths accepts = - (facts |> filter (member Thm.eq_thm ths o snd)) @ - (accepts |> filter_out (member Thm.eq_thm ths o snd)) + fun prepend_facts ths accepts = + ((facts |> filter (member Thm.eq_thm ths o snd)) @ + (accepts |> filter_out (member Thm.eq_thm ths o snd))) |> take max_relevant + fun append_facts ths accepts = + let val add = facts |> filter (member Thm.eq_thm ths o snd) in + (accepts |> filter_out (member Thm.eq_thm ths o snd) + |> take (max_relevant - length add)) @ + add + end fun uses_const s t = fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t false fun maybe_add_set_const (s, ths) accepts = accepts |> (if exists (uses_const s o prop_of o snd) accepts orelse exists (uses_const s) (concl_t :: hyp_ts) then - add_facts ths + append_facts ths else I) in facts |> map_filter (pair_consts_fact thy is_built_in_const fudge) |> iter 0 max_relevant threshold0 goal_const_tab [] - |> not (null add_ths) ? add_facts add_ths + |> not (null add_ths) ? prepend_facts add_ths |> (fn accepts => accepts |> could_benefit_from_ext is_built_in_const accepts - ? add_facts @{thms ext} + ? append_facts @{thms ext} |> fold maybe_add_set_const set_consts) |> tap (fn accepts => trace_msg ctxt (fn () => "Total relevant: " ^ string_of_int (length accepts)))