src/HOL/Tools/datatype_package.ML
changeset 18928 042608ffa2ec
parent 18857 c4b4fbd74ffb
child 18963 3adfc9dfb30a
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Feb 06 11:00:24 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Feb 06 11:01:28 2006 +0100
     1.3 @@ -564,7 +564,7 @@
     1.4        TYPE (msg, _, _) => error msg;
     1.5      val sorts' = add_typ_tfrees (T, sorts)
     1.6    in (Ts @ [T],
     1.7 -      case duplicates (map fst sorts') of
     1.8 +      case gen_duplicates (op =) (map fst sorts') of
     1.9           [] => sorts'
    1.10         | dups => error ("Inconsistent sort constraints for " ^ commas dups))
    1.11    end;
    1.12 @@ -956,14 +956,14 @@
    1.13      val (tyvars, _, _, _)::_ = dts;
    1.14      val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
    1.15        let val full_tname = Sign.full_name sign (Syntax.type_name tname mx)
    1.16 -      in (case duplicates tvs of
    1.17 +      in (case gen_duplicates (op =) tvs of
    1.18              [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
    1.19                    else error ("Mutually recursive datatypes must have same type parameters")
    1.20            | dups => error ("Duplicate parameter(s) for datatype " ^ full_tname ^
    1.21                " : " ^ commas dups))
    1.22        end) dts);
    1.23  
    1.24 -    val _ = (case duplicates (map fst new_dts) @ duplicates new_type_names of
    1.25 +    val _ = (case gen_duplicates (op =) (map fst new_dts) @ gen_duplicates (op =) new_type_names of
    1.26        [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
    1.27  
    1.28      fun prep_dt_spec ((dts', constr_syntax, sorts, i), (tvs, tname, mx, constrs)) =
    1.29 @@ -986,7 +986,7 @@
    1.30            Library.foldl prep_constr (([], [], sorts), constrs)
    1.31  
    1.32        in
    1.33 -        case duplicates (map fst constrs') of
    1.34 +        case gen_duplicates (op =) (map fst constrs') of
    1.35             [] =>
    1.36               (dts' @ [(i, (Sign.full_name sign (Syntax.type_name tname mx),
    1.37                  map DtTFree tvs, constrs'))],