src/HOL/Nominal/nominal_primrec.ML

 fun find_dts (dt_info : NominalDatatype.nominal_datatype_info Symtab.table) _ [] = []
   | find_dts dt_info tnames' (tname::tnames) =
       (case Symtab.lookup dt_info tname of
           NONE => primrec_err (quote tname ^ " is not a nominal datatype")
         | SOME dt =>
-            if gen_subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
+            if subset (op =) (tnames', map (#1 o snd) (#descr dt)) then
               (tname, dt)::(find_dts dt_info tnames' tnames)
             else find_dts dt_info tnames' tnames);
 
 fun common_prefix eq ([], _) = []
   | common_prefix eq (_, []) = []

       orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) spec' [];
     val dt_info = NominalDatatype.get_nominal_datatypes (ProofContext.theory_of lthy);
     val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
       map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
     val _ =
-      (if forall (curry (gen_eq_set (op =)) lsrs) lsrss andalso forall
+      (if forall (curry (eq_set (op =)) lsrs) lsrss andalso forall
          (fn (_, (_, _, (_, (ls, _, rs, _, _)) :: eqns)) =>
                forall (fn (_, (ls', _, rs', _, _)) =>
                  ls = ls' andalso rs = rs') eqns
            | _ => true) eqns
        then () else primrec_err param_err);

     val (fnames, fnss) = fold_rev (process_fun lthy descr eqns) main_fns ([], []);
     val (fs, defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []);
     val defs' = map (make_def lthy fixes fs) defs;
     val names1 = map snd fnames;
     val names2 = map fst eqns;
-    val _ = if gen_eq_set (op =) (names1, names2) then ()
+    val _ = if eq_set (op =) (names1, names2) then ()
       else primrec_err ("functions " ^ commas_quote names2 ^
         "\nare not mutually recursive");
     val (defs_thms, lthy') = lthy |>
       set_group ? LocalTheory.set_group (serial_string ()) |>
       fold_map (apfst (snd o snd) oo