src/ZF/Tools/datatype_package.ML

                    Syntax.string_of_term_global @{theory IFOL} t);
         val rec_names = (*nat doesn't have to be added*)
             @{const_name nat} :: map (#1 o dest_Const) rec_hds
         val u = if co then @{const QUniv.quniv} else @{const Univ.univ}
         val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
-          (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t
+          (fn t as Const (a, _) => if member (op =) rec_names a then I else insert (op =) t
             | _ => I)) con_ty_lists [];
     in  u $ Ind_Syntax.union_params (hd rec_tms, cs)  end;
 
 fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy =
  let

   (*Find each recursive argument and add a recursive call for it*)
   fun rec_args [] = []
     | rec_args ((Const(@{const_name mem},_)$arg$X)::prems) =
        (case head_of X of
             Const(a,_) => (*recursive occurrence?*)
-                          if a mem_string rec_names
+                          if member (op =) rec_names a
                               then arg :: rec_args prems
                           else rec_args prems
           | _ => rec_args prems)
     | rec_args (_::prems) = rec_args prems;