src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 53511 3ea6b9461c55
parent 53510 c0982ad1281d
child 53512 b9bc867e49f6
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
     1.3 @@ -18,7 +18,6 @@
     1.4       del : (Facts.ref * Attrib.src list) list,
     1.5       only : bool}
     1.6  
     1.7 -  val ignore_no_atp : bool Config.T
     1.8    val instantiate_inducts : bool Config.T
     1.9    val no_fact_override : fact_override
    1.10    val fact_of_ref :
    1.11 @@ -33,7 +32,6 @@
    1.12    val maybe_instantiate_inducts :
    1.13      Proof.context -> term list -> term -> (((unit -> string) * 'a) * thm) list
    1.14      -> (((unit -> string) * 'a) * thm) list
    1.15 -  val maybe_filter_no_atps : Proof.context -> ('a * thm) list -> ('a * thm) list
    1.16    val fact_of_raw_fact : raw_fact -> fact
    1.17    val all_facts :
    1.18      Proof.context -> bool -> bool -> unit Symtab.table -> thm list -> thm list
    1.19 @@ -59,9 +57,7 @@
    1.20     del : (Facts.ref * Attrib.src list) list,
    1.21     only : bool}
    1.22  
    1.23 -(* experimental features *)
    1.24 -val ignore_no_atp =
    1.25 -  Attrib.setup_config_bool @{binding sledgehammer_ignore_no_atp} (K false)
    1.26 +(* experimental feature *)
    1.27  val instantiate_inducts =
    1.28    Attrib.setup_config_bool @{binding sledgehammer_instantiate_inducts} (K false)
    1.29  
    1.30 @@ -245,7 +241,7 @@
    1.31    end
    1.32  
    1.33  fun is_blacklisted_or_something ctxt ho_atp name =
    1.34 -  (not (Config.get ctxt ignore_no_atp) andalso is_package_def name) orelse
    1.35 +  is_package_def name orelse
    1.36    exists (fn s => String.isSuffix s name) (multi_base_blacklist ctxt ho_atp)
    1.37  
    1.38  fun hackish_string_of_term ctxt =
    1.39 @@ -423,9 +419,6 @@
    1.40    else
    1.41      I
    1.42  
    1.43 -fun maybe_filter_no_atps ctxt =
    1.44 -  not (Config.get ctxt ignore_no_atp) ? filter_out (No_ATPs.member ctxt o snd)
    1.45 -
    1.46  fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th)
    1.47  
    1.48  fun all_facts ctxt generous ho_atp reserved add_ths chained css =
    1.49 @@ -511,8 +504,8 @@
    1.50         else
    1.51           let val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del) in
    1.52             all_facts ctxt false ho_atp reserved add chained css
    1.53 -           |> filter_out (member Thm.eq_thm_prop del o snd)
    1.54 -           |> maybe_filter_no_atps ctxt
    1.55 +           |> filter_out
    1.56 +                  ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
    1.57             |> hashed_keyed_distinct (size_of_term o prop_of o snd)
    1.58                    (normalize_eq_vars o prop_of o snd)
    1.59           end)