src/HOL/Tools/datatype_package.ML

   let
     val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle
       TYPE (msg, _, _) => error msg;
     val sorts' = add_typ_tfrees (T, sorts)
   in (Ts @ [T],
-      case gen_duplicates (op =) (map fst sorts') of
+      case duplicates (op =) (map fst sorts') of
          [] => sorts'
        | dups => error ("Inconsistent sort constraints for " ^ commas dups))
   end;
 
 

     val sign = Theory.sign_of tmp_thy;
 
     val (tyvars, _, _, _)::_ = dts;
     val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
       let val full_tname = Sign.full_name sign (Syntax.type_name tname mx)
-      in (case gen_duplicates (op =) tvs of
+      in (case duplicates (op =) tvs of
             [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
                   else error ("Mutually recursive datatypes must have same type parameters")
           | dups => error ("Duplicate parameter(s) for datatype " ^ full_tname ^
               " : " ^ commas dups))
       end) dts);
 
-    val _ = (case gen_duplicates (op =) (map fst new_dts) @ gen_duplicates (op =) new_type_names of
+    val _ = (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
       [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
 
     fun prep_dt_spec ((dts', constr_syntax, sorts, i), (tvs, tname, mx, constrs)) =
       let
         fun prep_constr ((constrs, constr_syntax', sorts'), (cname, cargs, mx')) =

 
         val (constrs', constr_syntax', sorts') =
           Library.foldl prep_constr (([], [], sorts), constrs)
 
       in
-        case gen_duplicates (op =) (map fst constrs') of
+        case duplicates (op =) (map fst constrs') of
            [] =>
              (dts' @ [(i, (Sign.full_name sign (Syntax.type_name tname mx),
                 map DtTFree tvs, constrs'))],
               constr_syntax @ [constr_syntax'], sorts', i + 1)
          | dups => error ("Duplicate constructors " ^ commas dups ^