--- a/src/HOL/TPTP/mash_export.ML Thu Dec 13 23:22:10 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML Thu Dec 13 23:47:01 2012 +0100
@@ -132,8 +132,7 @@
fun is_bad_query ctxt ho_atp th isar_deps =
Thm.legacy_get_kind th = "" orelse null isar_deps orelse
- is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th) orelse
- Sledgehammer_Fact.is_bad_for_atps ho_atp th
+ is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
fun generate_isar_or_prover_commands ctxt prover params_opt thys file_name =
let
@@ -179,7 +178,7 @@
val facts = all_facts ctxt
val (new_facts, old_facts) = facts |> List.partition (has_thys thys o snd)
val all_names = build_all_names nickname_of facts
- fun do_fact (fact as (_, th), old_facts) =
+ fun do_fact ((_, th), old_facts) =
let
val name = nickname_of th
val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Dec 13 23:22:10 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Thu Dec 13 23:47:01 2012 +0100
@@ -24,7 +24,6 @@
Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
-> Facts.ref * Attrib.src list -> ((string * stature) * thm) list
val backquote_thm : Proof.context -> thm -> string
- val is_bad_for_atps : bool -> thm -> bool
val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
val clasimpset_rule_table_of : Proof.context -> status Termtab.table
val build_all_names :
@@ -175,8 +174,8 @@
else
term_has_too_many_lambdas max_lambda_nesting t
-(* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31)
- was 11. *)
+(* The maximum apply depth of any "metis" call in "Metis_Examples" (on
+ 2007-10-31) was 11. *)
val max_apply_depth = 18
fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
@@ -210,7 +209,7 @@
andalso exists_subterm (fn Free (s, _) => s = Name.skolem Auto_Bind.thesisN
| _ => false) (prop_of th)
-fun is_likely_tautology_or_too_meta th =
+fun is_likely_tautology_too_meta_or_too_technical th =
let
fun is_interesting_subterm (Const (s, _)) =
not (member (op =) atp_widely_irrelevant_consts s)
@@ -229,14 +228,10 @@
| is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
is_boring_bool t andalso is_boring_bool u
| is_boring_prop _ _ = true
+ val t = prop_of th
in
- is_boring_prop [] (prop_of th) andalso
- not (Thm.eq_thm_prop (@{thm ext}, th))
- end
-
-fun is_bad_for_atps ho_atp th =
- let val t = prop_of th in
- is_too_complex ho_atp t orelse
+ (is_boring_prop [] (prop_of th) andalso
+ not (Thm.eq_thm_prop (@{thm ext}, th))) orelse
exists_type type_has_top_sort t orelse exists_technical_const t orelse
exists_low_level_class_const t orelse is_that_fact th
end
@@ -408,7 +403,7 @@
fun maybe_filter_no_atps ctxt =
not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
-fun all_facts ctxt really_all ho_atp reserved add_ths chained css =
+fun all_facts ctxt generous ho_atp reserved add_ths chained css =
let
val thy = Proof_Context.theory_of ctxt
val global_facts = Global_Theory.facts_of thy
@@ -429,7 +424,7 @@
forall (not o member Thm.eq_thm_prop add_ths) ths andalso
(Facts.is_concealed facts name0 orelse
not (can (Proof_Context.get_thms ctxt) name0) orelse
- (not really_all andalso
+ (not generous andalso
is_blacklisted_or_something ctxt ho_atp name0)) then
I
else
@@ -445,8 +440,9 @@
#> fold_rev (fn th => fn (j, (multis, unis)) =>
(j - 1,
if not (member Thm.eq_thm_prop add_ths th) andalso
- is_likely_tautology_or_too_meta th orelse
- (not really_all andalso is_bad_for_atps ho_atp th) then
+ (is_likely_tautology_too_meta_or_too_technical th orelse
+ (not generous andalso
+ is_too_complex ho_atp (prop_of th))) then
(multis, unis)
else
let