src/HOL/Tools/record_package.ML

     val err_dup_record =
       if is_none (get_record thy name) then []
       else ["Duplicate definition of record " ^ quote name];
 
     val err_dup_parms =
-      (case duplicates params of
+      (case gen_duplicates (op =) params of
         [] => []
       | dups => ["Duplicate parameter(s) " ^ commas dups]);
 
     val err_extra_frees =
       (case gen_rems (op =) (envir_names, params) of

       | extras => ["Extra free type variable(s) " ^ commas extras]);
 
     val err_no_fields = if null bfields then ["No fields present"] else [];
 
     val err_dup_fields =
-      (case duplicates (map #1 bfields) of
+      (case gen_duplicates (op =) (map #1 bfields) of
         [] => []
       | dups => ["Duplicate field(s) " ^ commas_quote dups]);
 
     val err_bad_fields =
       if forall (not_equal moreN o #1) bfields then []
       else ["Illegal field name " ^ quote moreN];
 
     val err_dup_sorts =
-      (case duplicates envir_names of
+      (case gen_duplicates (op =) envir_names of
         [] => []
       | dups => ["Inconsistent sort constraints for " ^ commas dups]);
 
     val errs =
       err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @