src/HOL/Tools/res_atp.ML
changeset 24854 0ebcd575d3c6
parent 24827 646bdc51eb7d
child 24867 e5b55d7be9bb
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Oct 05 08:38:09 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Oct 05 09:59:03 2007 +0200
     1.3 @@ -606,12 +606,9 @@
     1.4    | add_single_names ((a, [th]), pairs) = (a,th)::pairs
     1.5    | add_single_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
     1.6  
     1.7 -val multi_base_blacklist =
     1.8 -  ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"];
     1.9 -
    1.10  (*Ignore blacklisted basenames*)
    1.11  fun add_multi_names ((a, ths), pairs) =
    1.12 -  if (Sign.base_name a) mem_string multi_base_blacklist  then pairs
    1.13 +  if (Sign.base_name a) mem_string ResAxioms.multi_base_blacklist  then pairs
    1.14    else add_single_names ((a, ths), pairs);
    1.15  
    1.16  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;