src/HOL/Tools/refute.ML

   let
     val class_const_names = map Logic.const_of_class (Sign.all_classes thy)
   in
     (* I'm not quite sure if checking the name 's' is sufficient, *)
     (* or if we should also check the type 'T'.                   *)
-    s mem_string class_const_names
+    member (op =) class_const_names s
   end;
 
 (* ------------------------------------------------------------------------- *)
 (* is_IDT_constructor: returns 'true' iff 'Const (s, T)' is the constructor  *)
 (*                     of an inductive datatype in 'thy'                     *)

     val rec_names = Symtab.fold (append o #rec_names o snd)
       (Datatype.get_all thy) []
   in
     (* I'm not quite sure if checking the name 's' is sufficient, *)
     (* or if we should also check the type 'T'.                   *)
-    s mem_string rec_names
+    member (op =) rec_names s
   end;
 
 (* ------------------------------------------------------------------------- *)
 (* norm_rhs: maps  f ?t1 ... ?tn == rhs  to  %t1...tn. rhs                   *)
 (* ------------------------------------------------------------------------- *)

                 Datatype_Aux.DtTFree _ =>
                 collect_types dT acc
               | Datatype_Aux.DtType (_, ds) =>
                 collect_types dT (fold_rev collect_dtyp ds acc)
               | Datatype_Aux.DtRec i =>
-                if dT mem acc then
+                if member (op =) acc dT then
                   acc  (* prevent infinite recursion *)
                 else
                   let
                     val (_, dtyps, dconstrs) = the (AList.lookup (op =) descr i)
                     (* if the current type is a recursive IDT (i.e. a depth *)

                       val (intrs, new_offset) =
                         fold_map (fn t_elem => fn off =>
                           (* if 't_elem' existed at the previous depth,    *)
                           (* proceed recursively, otherwise map the entire *)
                           (* subtree to "undefined"                        *)
-                          if t_elem mem terms' then
+                          if member (op =) terms' t_elem then
                             make_constr ds off
                           else
                             (make_undef ds, off))
                         terms offset
                     in