src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML

   type fact_override =
     {add : (Facts.ref * Attrib.src list) list,
      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 :
     Proof.context -> unit Symtab.table -> thm list -> status Termtab.table
     -> Facts.ref * Attrib.src list -> ((string * stature) * thm) list

     (thm -> string) -> ('a * thm) list
     -> string Symtab.table * string Symtab.table
   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
     -> status Termtab.table -> raw_fact list
   val nearly_all_facts :

 type fact_override =
   {add : (Facts.ref * Attrib.src list) list,
    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)
 
 val no_fact_override = {add = [], del = [], only = false}
 

     exists_Const (is_technical_const orf is_low_level_class_const) t orelse
     is_that_fact th
   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 =
   with_vanilla_print_mode (Syntax.string_of_term ctxt) #> simplify_spaces
 

         |> Logic.list_implies |> Object_Logic.atomize_term thy
       val ind_stmt_xs = external_frees ind_stmt
     in maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) end
   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 =
   let

          maps (map (fn ((name, stature), th) => ((K name, stature), th))
                o fact_of_ref ctxt reserved chained css) add
        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)
       |> maybe_instantiate_inducts ctxt hyp_ts concl_t
     end