src/HOL/Tools/res_atp.ML
changeset 24854 0ebcd575d3c6
parent 24827 646bdc51eb7d
child 24867 e5b55d7be9bb
equal deleted inserted replaced
24853:aab5798e5a33 24854:0ebcd575d3c6
   604 
   604 
   605 fun add_single_names ((a, []), pairs) = pairs
   605 fun add_single_names ((a, []), pairs) = pairs
   606   | add_single_names ((a, [th]), pairs) = (a,th)::pairs
   606   | add_single_names ((a, [th]), pairs) = (a,th)::pairs
   607   | add_single_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
   607   | add_single_names ((a, ths), pairs) = #2 (foldl (multi_name a) (1,pairs) ths);
   608 
   608 
   609 val multi_base_blacklist =
       
   610   ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm"];
       
   611 
       
   612 (*Ignore blacklisted basenames*)
   609 (*Ignore blacklisted basenames*)
   613 fun add_multi_names ((a, ths), pairs) =
   610 fun add_multi_names ((a, ths), pairs) =
   614   if (Sign.base_name a) mem_string multi_base_blacklist  then pairs
   611   if (Sign.base_name a) mem_string ResAxioms.multi_base_blacklist  then pairs
   615   else add_single_names ((a, ths), pairs);
   612   else add_single_names ((a, ths), pairs);
   616 
   613 
   617 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   614 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   618 
   615 
   619 (*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)
   616 (*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)