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 tnames' subset (map (#1 o snd) (#descr dt)) then
+            if gen_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 eq_set lsrs) lsrss andalso forall
+      (if forall (curry (gen_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);