src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
changeset 36692 54b64d4ad524
parent 36550 f8da913b6c3a
child 36922 12f87df9c1a5
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -387,7 +387,7 @@
     1.4  
     1.5  (*Ignore blacklisted basenames*)
     1.6  fun add_multi_names (a, ths) pairs =
     1.7 -  if (Long_Name.base_name a) mem_string multi_base_blacklist then pairs
     1.8 +  if member (op =) multi_base_blacklist (Long_Name.base_name a) then pairs
     1.9    else add_single_names (a, ths) pairs;
    1.10  
    1.11  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;