--- 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)