# HG changeset patch
# User blanchet
# Date 1325511140 -3600
# Node ID b2594cc862d7100175745a2228cadac731393d9c
# Parent  291c14a01b6d1aebd9d4318d6761bc69b09a4c5b
removed special handling for set constants in relevance filter

diff -r 291c14a01b6d -r b2594cc862d7 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Jan 02 14:26:57 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Jan 02 14:32:20 2012 +0100
@@ -223,9 +223,7 @@
 
 (*** constants with types ***)
 
-fun order_of_type (Type (@{type_name fun}, [T1, @{typ bool}])) =
-    order_of_type T1 (* cheat: pretend sets are first-order *)
-  | order_of_type (Type (@{type_name fun}, [T1, T2])) =
+fun order_of_type (Type (@{type_name fun}, [T1, T2])) =
     Int.max (order_of_type T1 + 1, order_of_type T2)
   | order_of_type (Type (_, Ts)) = fold (Integer.max o order_of_type) Ts 0
   | order_of_type _ = 0
@@ -279,15 +277,6 @@
   if (not also_skolem andalso String.isPrefix skolem_prefix s) then I
   else Symtab.map_default (s, [p]) (insert (op =) p)
 
-(* 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
-   definition at the end. *)
-val set_consts =
-  [(@{const_name Collect}, []),
-   (@{const_name Set.member}, [])]
-
-val is_set_const = AList.defined (op =) set_consts
-
 fun add_pconsts_in_term thy is_built_in_const also_skolems pos =
   let
     val flip = Option.map not
@@ -295,19 +284,16 @@
        each quantifiers that must necessarily be skolemized by the automatic
        prover, we introduce a fresh constant to simulate the effect of
        Skolemization. *)
-    fun do_const const ext_arg (x as (s, _)) ts =
+    fun do_const const x ts =
       let val (built_in, ts) = is_built_in_const x ts in
-        if is_set_const s then
-          fold (do_term ext_arg) ts
-        else
-          (not built_in
-           ? add_pconst_to_table also_skolems (rich_pconst thy const x))
-          #> fold (do_term false) ts
+        (not built_in
+         ? add_pconst_to_table also_skolems (rich_pconst thy const x))
+        #> fold (do_term false) ts
       end
     and do_term ext_arg t =
       case strip_comb t of
-        (Const x, ts) => do_const true ext_arg x ts
-      | (Free x, ts) => do_const false ext_arg x ts
+        (Const x, ts) => do_const true x ts
+      | (Free x, ts) => do_const false x ts
       | (Abs (_, T, t'), ts) =>
         ((null ts andalso not ext_arg)
          (* Since lambdas on the right-hand side of equalities are usually
@@ -678,15 +664,6 @@
       ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
        (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
       |> take max_relevant
-    fun uses_const s t =
-      fold_aterms (curry (fn (Const (s', _), false) => s' = s | (_, b) => b)) t
-                  false
-    fun add_set_const_thms accepts (s, ths) =
-      if exists (uses_const s o prop_of o snd) accepts orelse
-         exists (uses_const s) (concl_t :: hyp_ts) then
-        append ths
-      else
-        I
     fun insert_into_facts accepts [] = accepts
       | insert_into_facts accepts ths =
         let
@@ -698,7 +675,6 @@
         in bef @ add @ after end
     fun insert_special_facts accepts =
        [] |> could_benefit_from_ext is_built_in_const accepts ? cons @{thm ext}
-          |> fold (add_set_const_thms accepts) set_consts
           |> insert_into_facts accepts
   in
     facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)