src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

   | is_unit_equality _ = false
 
 fun is_appropriate_prop_of_prover ctxt name =
   if is_unit_equational_atp ctxt name then is_unit_equality else K true
 
+val atp_irrelevant_const_tab =
+  Symtab.make (map (rpair ()) atp_irrelevant_consts)
+
 fun is_built_in_const_of_prover ctxt name =
   if is_smt_prover ctxt name then
     let val ctxt = ctxt |> select_smt_solver name in
       fn x => fn ts =>
          if SMT_Builtin.is_builtin_num_ext ctxt (list_comb (Const x, ts)) then

            (true, ts)
          else
            (false, ts)
     end
   else
-    fn (s, _) => fn ts => (member (op =) atp_irrelevant_consts s, ts)
+    fn (s, _) => fn ts => (Symtab.defined atp_irrelevant_const_tab s, ts)
 
 (* FUDGE *)
 val atp_relevance_fudge =
   {local_const_multiplier = 1.5,
    worse_irrel_freq = 100.0,