# HG changeset patch
# User blanchet
# Date 1337254583 -7200
# Node ID 9ff976a6c2cb48839026de32cc0d352a0081cbcd
# Parent  2924f37cb6b38ae6cf70ab9105dae993dc10ae65
added "Collect_cong" to cover extensionality of "Collect" (special cases of "ext" pass through the relevant filter)

diff -r 2924f37cb6b3 -r 9ff976a6c2cb src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Wed May 16 19:20:19 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Thu May 17 13:36:23 2012 +0200
@@ -366,7 +366,7 @@
    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
@@ -777,6 +777,7 @@
                     |> 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