src/HOL/Tools/old_primrec.ML

           |-> (fn t' => pair (Abs (a, T, t')))
       | subst subs (t as (_ $ _)) fs =
           let
             val (f, ts) = strip_comb t;
           in
-            if is_Const f andalso dest_Const f mem map fst rec_eqns then
+            if is_Const f andalso member (op =) (map fst rec_eqns) (dest_Const f) then
               let
                 val fnameT' as (fname', _) = dest_Const f;
                 val (_, rpos, _) = the (AList.lookup (op =) rec_eqns fnameT');
                 val ls = take rpos ts;
                 val rest = drop rpos ts;