src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML

 
 (* Set constants tend to pull in too many irrelevant facts. We limit the damage
    by treating them more or less as if they were built-in but add their
    axiomatization at the end. *)
 val set_consts = [@{const_name Collect}, @{const_name Set.member}]
-val set_thms = @{thms Collect_mem_eq mem_Collect_eq}
+val set_thms = @{thms Collect_mem_eq mem_Collect_eq Collect_cong}
 
 fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
   let
     val flip = Option.map not
     (* We include free variables, as well as constants, to handle locales. For

             accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
                     |> take (max_relevant - length add)
                     |> chop special_fact_index
         in bef @ add @ after end
     fun insert_special_facts accepts =
+       (* FIXME: get rid of "ext" here once it is treated as a helper *)
        [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
           |> add_set_const_thms accepts
           |> insert_into_facts accepts
   in
     facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)