1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed May 16 18:16:51 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed May 16 18:16:51 2012 +0200
     1.3 @@ -362,6 +362,12 @@
     1.4    if (not also_skolem andalso String.isPrefix skolem_prefix s) then I
     1.5    else Symtab.map_default (s, [p]) (insert (op =) p)
     1.6  
     1.7 +(* Set constants tend to pull in too many irrelevant facts. We limit the damage
     1.8 +   by treating them more or less as if they were built-in but add their
     1.9 +   axiomatization at the end. *)
    1.10 +val set_consts = [@{const_name Collect}, @{const_name Set.member}]
    1.11 +val set_thms = @{thms Collect_mem_eq mem_Collect_eq}
    1.12 +
    1.13  fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
    1.14    let
    1.15      val flip = Option.map not
    1.16 @@ -369,16 +375,19 @@
    1.17         each quantifiers that must necessarily be skolemized by the automatic
    1.18         prover, we introduce a fresh constant to simulate the effect of
    1.19         Skolemization. *)
    1.20 -    fun do_const const x ts =
    1.21 +    fun do_const const ext_arg (x as (s, _)) ts =
    1.22        let val (built_in, ts) = is_built_in_const x ts in
    1.23 -        (not built_in
    1.24 -         ? add_pconst_to_table also_skolems (rich_pconst thy const x))
    1.25 -        #> fold (do_term false) ts
    1.26 +        if member (op =) set_consts s then
    1.27 +          fold (do_term ext_arg) ts
    1.28 +        else
    1.29 +          (not built_in
    1.30 +           ? add_pconst_to_table also_skolems (rich_pconst thy const x))
    1.31 +          #> fold (do_term false) ts
    1.32        end
    1.33      and do_term ext_arg t =
    1.34        case strip_comb t of
    1.35 -        (Const x, ts) => do_const true x ts
    1.36 -      | (Free x, ts) => do_const false x ts
    1.37 +        (Const x, ts) => do_const true ext_arg x ts
    1.38 +      | (Free x, ts) => do_const false ext_arg x ts
    1.39        | (Abs (_, T, t'), ts) =>
    1.40          ((null ts andalso not ext_arg)
    1.41           (* Since lambdas on the right-hand side of equalities are usually
    1.42 @@ -750,6 +759,14 @@
    1.43        ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
    1.44         (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
    1.45        |> take max_relevant
    1.46 +    fun uses_const s t =
    1.47 +      fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
    1.48 +                  false
    1.49 +    fun uses_const_anywhere accepts s =
    1.50 +      exists (uses_const s o prop_of o snd) accepts orelse
    1.51 +      exists (uses_const s) (concl_t :: hyp_ts)
    1.52 +    fun add_set_const_thms accepts =
    1.53 +      exists (uses_const_anywhere accepts) set_consts ? append set_thms
    1.54      fun insert_into_facts accepts [] = accepts
    1.55        | insert_into_facts accepts ths =
    1.56          let
    1.57 @@ -761,6 +778,7 @@
    1.58          in bef @ add @ after end
    1.59      fun insert_special_facts accepts =
    1.60         [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
    1.61 +          |> add_set_const_thms accepts
    1.62            |> insert_into_facts accepts
    1.63    in
    1.64      facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)