diff -r 75786c2eb897 -r bc5c6c9b114e src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Feb 15 19:11:10 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Feb 15 21:34:55 2006 +0100
@@ -326,7 +326,7 @@
 fun dt_cases (descr: descr) (_, args, constrs) =
   let
     fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
-    val bnames = map the_bname (distinct (List.concat (map dt_recs args)));
+    val bnames = map the_bname (distinct (op =) (List.concat (map dt_recs args)));
   in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
 
 
@@ -492,7 +492,7 @@
             ([], true, SOME _) =>
               case_error "Extra '_' dummy pattern" (SOME tname) [u]
           | (_ :: _, _, _) =>
-              let val extra = distinct (map (fst o fst) cases'')
+              let val extra = distinct (op =) (map (fst o fst) cases'')
               in case extra \\ map fst constrs of
                   [] => case_error ("More than one clause for constructor(s) " ^
                     commas extra) (SOME tname) [u]