--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sun May 01 18:37:25 2011 +0200
@@ -777,17 +777,17 @@
(* Facts containing variables of type "unit" or "bool" or of the form
"ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
are omitted. *)
-fun is_dangerous_term half_sound t =
- not half_sound andalso
+fun is_dangerous_term fairly_sound t =
+ not fairly_sound andalso
let val t = transform_elim_term t in
has_bound_or_var_of_type dangerous_types t orelse
is_exhaustive_finite t
end
-fun is_theorem_bad_for_atps half_sound thm =
+fun is_theorem_bad_for_atps fairly_sound thm =
let val t = prop_of thm in
is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
- is_dangerous_term half_sound t orelse exists_sledgehammer_const t orelse
+ is_dangerous_term fairly_sound t orelse exists_sledgehammer_const t orelse
exists_low_level_class_const t orelse is_metastrange_theorem thm orelse
is_that_fact thm
end
@@ -800,7 +800,7 @@
val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd
in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end
-fun all_facts ctxt reserved really_all half_sound
+fun all_facts ctxt reserved really_all fairly_sound
({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge)
add_ths chained_ths =
let
@@ -846,7 +846,7 @@
pair 1
#> fold (fn th => fn (j, rest) =>
(j + 1,
- if is_theorem_bad_for_atps half_sound th andalso
+ if is_theorem_bad_for_atps fairly_sound th andalso
not (member Thm.eq_thm add_ths th) then
rest
else
@@ -890,7 +890,7 @@
fun external_frees t =
[] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
-fun relevant_facts ctxt half_sound (threshold0, threshold1) max_relevant
+fun relevant_facts ctxt fairly_sound (threshold0, threshold1) max_relevant
is_built_in_const fudge (override as {add, only, ...})
chained_ths hyp_ts concl_t =
let
@@ -908,7 +908,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 half_sound fudge add_ths chained_ths)
+ all_facts ctxt reserved false fairly_sound fudge add_ths chained_ths)
|> instantiate_inducts
? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
|> rearrange_facts ctxt (respect_no_atp andalso not only)