src/HOL/Tools/datatype_package.ML
changeset 19046 bc5c6c9b114e
parent 19008 14c1b2f5dda4
child 19346 c4c003abd830
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Feb 15 19:11:10 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Feb 15 21:34:55 2006 +0100
     1.3 @@ -326,7 +326,7 @@
     1.4  fun dt_cases (descr: descr) (_, args, constrs) =
     1.5    let
     1.6      fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
     1.7 -    val bnames = map the_bname (distinct (List.concat (map dt_recs args)));
     1.8 +    val bnames = map the_bname (distinct (op =) (List.concat (map dt_recs args)));
     1.9    in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
    1.10  
    1.11  
    1.12 @@ -492,7 +492,7 @@
    1.13              ([], true, SOME _) =>
    1.14                case_error "Extra '_' dummy pattern" (SOME tname) [u]
    1.15            | (_ :: _, _, _) =>
    1.16 -              let val extra = distinct (map (fst o fst) cases'')
    1.17 +              let val extra = distinct (op =) (map (fst o fst) cases'')
    1.18                in case extra \\ map fst constrs of
    1.19                    [] => case_error ("More than one clause for constructor(s) " ^
    1.20                      commas extra) (SOME tname) [u]