--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue May 24 00:01:33 2011 +0200
@@ -785,9 +785,9 @@
(**** Predicates to detect unwanted facts (prolific or likely to cause
unsoundness) ****)
-fun is_theorem_bad_for_atps is_good_prop thm =
+fun is_theorem_bad_for_atps is_appropriate_prop thm =
let val t = prop_of thm in
- not (is_good_prop t) orelse is_formula_too_complex t orelse
+ not (is_appropriate_prop t) orelse is_formula_too_complex t orelse
exists_type type_has_top_sort t orelse exists_sledgehammer_const t orelse
exists_low_level_class_const t orelse is_metastrange_theorem thm orelse
is_that_fact thm
@@ -815,7 +815,7 @@
mk_fact_table normalize_simp_prop snd simps)
end
-fun all_facts ctxt reserved really_all is_good_prop add_ths chained_ths =
+fun all_facts ctxt reserved really_all is_appropriate_prop add_ths chained_ths =
let
val thy = Proof_Context.theory_of ctxt
val global_facts = Global_Theory.facts_of thy
@@ -869,8 +869,8 @@
pair 1
#> fold (fn th => fn (j, rest) =>
(j + 1,
- if is_theorem_bad_for_atps is_good_prop th andalso
- not (member Thm.eq_thm add_ths th) then
+ if not (member Thm.eq_thm add_ths th) andalso
+ is_theorem_bad_for_atps is_appropriate_prop th then
rest
else
(((fn () =>
@@ -903,9 +903,9 @@
fun external_frees t =
[] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
-fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_good_prop
- is_built_in_const fudge (override as {add, only, ...})
- chained_ths hyp_ts concl_t =
+fun relevant_facts ctxt (threshold0, threshold1) max_relevant
+ is_appropriate_prop is_built_in_const fudge
+ (override as {add, only, ...}) chained_ths hyp_ts concl_t =
let
val thy = Proof_Context.theory_of ctxt
val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
@@ -921,7 +921,7 @@
maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
o fact_from_ref ctxt reserved chained_ths) add
else
- all_facts ctxt reserved false is_good_prop add_ths chained_ths)
+ all_facts ctxt reserved false is_appropriate_prop add_ths chained_ths)
|> Config.get ctxt instantiate_inducts
? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
|> rearrange_facts ctxt only