--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Wed May 05 18:25:34 2010 +0200
@@ -387,7 +387,7 @@
(*Ignore blacklisted basenames*)
fun add_multi_names (a, ths) pairs =
- if (Long_Name.base_name a) mem_string multi_base_blacklist then pairs
+ if member (op =) multi_base_blacklist (Long_Name.base_name a) then pairs
else add_single_names (a, ths) pairs;
fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;