# HG changeset patch
# User blanchet
# Date 1355438821 -3600
# Node ID 0799339fea0f3cdf961a3c6f1bf3b48a68fec48b
# Parent  19dbd75540767268e47ec20a50acdb9f1f2215ff
get rid of some junk facts in the MaSh evaluation driver

diff -r 19dbd7554076 -r 0799339fea0f src/HOL/TPTP/mash_export.ML
--- 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
diff -r 19dbd7554076 -r 0799339fea0f src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- 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