# HG changeset patch
# User blanchet
# Date 1378821411 -7200
# Node ID 3ea6b9461c55d055194c33195e5daa02fdb73706
# Parent  c0982ad1281d9c797af80f545a4d0a77ba25891b
got rid of another slowdown factor in relevance filter

diff -r c0982ad1281d -r 3ea6b9461c55 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
@@ -18,7 +18,6 @@
      del : (Facts.ref * Attrib.src list) list,
      only : bool}
 
-  val ignore_no_atp : bool Config.T
   val instantiate_inducts : bool Config.T
   val no_fact_override : fact_override
   val fact_of_ref :
@@ -33,7 +32,6 @@
   val maybe_instantiate_inducts :
     Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
     -> (((unit -> string) * 'a) * thm) list
-  val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
   val fact_of_raw_fact : raw_fact -> fact
   val all_facts :
     Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list
@@ -59,9 +57,7 @@
    del : (Facts.ref * Attrib.src list) list,
    only : bool}
 
-(* experimental features *)
-val ignore_no_atp =
-  Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
+(* experimental feature *)
 val instantiate_inducts =
   Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
 
@@ -245,7 +241,7 @@
   end
 
 fun is_blacklisted_or_something ctxt ho_atp name =
-  (not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse
+  is_package_def name orelse
   exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp)
 
 fun hackish_string_of_term ctxt =
@@ -423,9 +419,6 @@
   else
     I
 
-fun maybe_filter_no_atps ctxt =
-  not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
-
 fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th)
 
 fun all_facts ctxt generous ho_atp reserved add_ths chained css =
@@ -511,8 +504,8 @@
        else
          let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
            all_facts ctxt false ho_atp reserved add chained css
-           |> filter_out (member Thm.eq_thm_prop del o snd)
-           |> maybe_filter_no_atps ctxt
+           |> filter_out
+                  ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
            |> hashed_keyed_distinct (size_of_term o prop_of o snd)
                   (normalize_eq_vars o prop_of o snd)
          end)