src/HOL/Tools/hologic.ML

 fun ptuple_err s = raise TERM (s ^ ": inconsistent use of nested products", []);
 
 fun mk_ptupleT ps =
   let
     fun mk p Ts =
-      if p mem ps then
+      if member (op =) ps p then
         let
           val (T, Ts') = mk (1::p) Ts;
           val (U, Ts'') = mk (2::p) Ts'
         in (mk_prodT (T, U), Ts'') end
       else (hd Ts, tl Ts)
   in fst o mk [] end;
 
 fun strip_ptupleT ps =
   let
-    fun factors p T = if p mem ps then (case T of
+    fun factors p T = if member (op =) ps p then (case T of
         Type ("*", [T1, T2]) =>
           factors (1::p) T1 @ factors (2::p) T2
       | _ => ptuple_err "strip_ptupleT") else [T]
   in factors [] end;
 

   in factors [] end;
 
 fun mk_ptuple ps =
   let
     fun mk p T ts =
-      if p mem ps then (case T of
+      if member (op =) ps p then (case T of
           Type ("*", [T1, T2]) =>
             let
               val (t, ts') = mk (1::p) T1 ts;
               val (u, ts'') = mk (2::p) T2 ts'
             in (pair_const T1 T2 $ t $ u, ts'') end

       else (hd ts, tl ts)
   in fst oo mk [] end;
 
 fun strip_ptuple ps =
   let
-    fun dest p t = if p mem ps then (case t of
+    fun dest p t = if member (op =) ps p then (case t of
         Const ("Pair", _) $ t $ u =>
           dest (1::p) t @ dest (2::p) u
       | _ => ptuple_err "strip_ptuple") else [t]
   in dest [] end;
 

   with result type T.  The call creates a new term expecting one argument
   of type S.*)
 fun mk_psplits ps T T3 u =
   let
     fun ap ((p, T) :: pTs) =
-          if p mem ps then (case T of
+          if member (op =) ps p then (case T of
               Type ("*", [T1, T2]) =>
                 split_const (T1, T2, map snd pTs ---> T3) $
                   ap ((1::p, T1) :: (2::p, T2) :: pTs)
             | _ => ptuple_err "mk_psplits")
           else Abs ("x", T, ap pTs)