renamed gen_duplicates to duplicates;

--- a/src/HOL/Tools/datatype_package.ML	Tue Feb 07 08:47:43 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Tue Feb 07 19:56:45 2006 +0100
@@ -540,7 +540,7 @@
       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;
@@ -932,14 +932,14 @@
     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)) =
@@ -962,7 +962,7 @@
           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'))],

--- a/src/HOL/Tools/inductive_codegen.ML	Tue Feb 07 08:47:43 2006 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Tue Feb 07 19:56:45 2006 +0100
@@ -231,7 +231,7 @@
             val (in_ts, out_ts) = get_args is 1 us;
             val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
             val vTs = List.concat (map term_vTs out_ts');
-            val dupTs = map snd (gen_duplicates (op =) vTs) @
+            val dupTs = map snd (duplicates (op =) vTs) @
               List.mapPartial (AList.lookup (op =) vTs) vs;
           in
             terms_vs (in_ts @ in_ts') subset vs andalso
@@ -258,7 +258,7 @@
     val in_vs = terms_vs in_ts;
     val concl_vs = terms_vs ts
   in
-    forall is_eqT (map snd (gen_duplicates (op =) (List.concat (map term_vTs in_ts)))) andalso
+    forall is_eqT (map snd (duplicates (op =) (List.concat (map term_vTs in_ts)))) andalso
     forall (is_eqT o fastype_of) in_ts' andalso
     (case check_mode_prems (arg_vs union in_vs) ps of
        NONE => false

--- a/src/HOL/Tools/primrec_package.ML	Tue Feb 07 08:47:43 2006 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Tue Feb 07 19:56:45 2006 +0100
@@ -69,7 +69,7 @@
     if length middle > 1 then 
       raise RecError "more than one non-variable in pattern"
     else
-     (check_vars "repeated variable names in pattern: " (gen_duplicates (op =) lfrees);
+     (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
       check_vars "extra variables on rhs: "
         (map dest_Free (term_frees rhs) \\ lfrees);
       case AList.lookup (op =) rec_fns fnameT of

--- a/src/HOL/Tools/record_package.ML	Tue Feb 07 08:47:43 2006 +0100
+++ b/src/HOL/Tools/record_package.ML	Tue Feb 07 19:56:45 2006 +0100
@@ -2060,7 +2060,7 @@
       else ["Duplicate definition of record " ^ quote name];
 
     val err_dup_parms =
-      (case gen_duplicates (op =) params of
+      (case duplicates (op =) params of
         [] => []
       | dups => ["Duplicate parameter(s) " ^ commas dups]);
 
@@ -2072,7 +2072,7 @@
     val err_no_fields = if null bfields then ["No fields present"] else [];
 
     val err_dup_fields =
-      (case gen_duplicates (op =) (map #1 bfields) of
+      (case duplicates (op =) (map #1 bfields) of
         [] => []
       | dups => ["Duplicate field(s) " ^ commas_quote dups]);
 
@@ -2081,7 +2081,7 @@
       else ["Illegal field name " ^ quote moreN];
 
     val err_dup_sorts =
-      (case gen_duplicates (op =) envir_names of
+      (case duplicates (op =) envir_names of
         [] => []
       | dups => ["Inconsistent sort constraints for " ^ commas dups]);
 

--- a/src/HOL/Tools/typedef_package.ML	Tue Feb 07 08:47:43 2006 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Tue Feb 07 19:56:45 2006 +0100
@@ -200,7 +200,7 @@
       else ["Illegal schematic variable(s) on rhs"];
 
     val dup_lhs_tfrees =
-      (case gen_duplicates (op =) lhs_tfrees of [] => []
+      (case duplicates (op =) lhs_tfrees of [] => []
       | dups => ["Duplicate type variables on lhs: " ^ show_names dups]);
 
     val extra_rhs_tfrees =

--- a/src/HOLCF/domain/extender.ML	Tue Feb 07 08:47:43 2006 +0100
+++ b/src/HOLCF/domain/extender.ML	Tue Feb 07 19:56:45 2006 +0100
@@ -43,15 +43,15 @@
      cons'' : ((string * mixfix * (bool * string option * typ) list) list) list) sg =
   let
     val defaultS = Sign.defaultS sg;
-    val test_dupl_typs = (case gen_duplicates (op =) (map fst dtnvs) of 
+    val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of 
 	[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
-    val test_dupl_cons = (case gen_duplicates (op =) (map first (List.concat cons'')) of 
+    val test_dupl_cons = (case duplicates (op =) (map first (List.concat cons'')) of 
 	[] => false | dups => error ("Duplicate constructors: " 
 							 ^ commas_quote dups));
-    val test_dupl_sels = (case gen_duplicates (op =) (List.mapPartial second
+    val test_dupl_sels = (case duplicates (op =) (List.mapPartial second
 			       (List.concat (map third (List.concat cons'')))) of
         [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
-    val test_dupl_tvars = exists(fn s=>case gen_duplicates (op =) (map(fst o dest_TFree)s)of
+    val test_dupl_tvars = exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
 	[] => false | dups => error("Duplicate type arguments: " 
 		   ^commas_quote dups)) (map snd dtnvs);
     (* test for free type variables, illegal sort constraints on rhs,

--- a/src/Pure/Isar/locale.ML	Tue Feb 07 08:47:43 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Feb 07 19:56:45 2006 +0100
@@ -675,7 +675,7 @@
 
     fun rename_parms top ren ((name, ps), (parms, mode)) =
       let val ps' = map (Element.rename ren) ps in
-        (case duplicates ps' of
+        (case duplicates (op =) ps' of
           [] => ((name, ps'),
                  if top then (map (Element.rename ren) parms,
                    map_mode (map (fn (t, th) =>

--- a/src/Pure/Isar/session.ML	Tue Feb 07 08:47:43 2006 +0100
+++ b/src/Pure/Isar/session.ML	Tue Feb 07 19:56:45 2006 +0100
@@ -41,7 +41,7 @@
 
 fun add_path reset s =
   let val sess = ! session @ [s] in
-    (case gen_duplicates (op =) sess of
+    (case duplicates (op =) sess of
       [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
     | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
   end;

--- a/src/Pure/Syntax/syntax.ML	Tue Feb 07 08:47:43 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML	Tue Feb 07 19:56:45 2006 +0100
@@ -127,7 +127,7 @@
         val trs2 = these (AList.lookup (op =) tabs2 mode);
         val trs = gen_distinct eq_tr (trs1 @ trs2);
       in
-        (case gen_duplicates (eq_fst (op =)) trs of
+        (case duplicates (eq_fst (op =)) trs of
           [] => (mode, trs)
         | dups => error ("More than one token translation function in mode " ^
             quote mode ^ " for " ^ commas_quote (map name dups)))

--- a/src/Pure/axclass.ML	Tue Feb 07 08:47:43 2006 +0100
+++ b/src/Pure/axclass.ML	Tue Feb 07 19:56:45 2006 +0100
@@ -99,7 +99,7 @@
         Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ())
       | _ => err ());
     val ss =
-      if null (gen_duplicates (eq_fst (op =)) tvars)
+      if null (duplicates (eq_fst (op =)) tvars)
       then map snd tvars else err ();
   in (t, ss, c) end;
 

--- a/src/Pure/logic.ML	Tue Feb 07 08:47:43 2006 +0100
+++ b/src/Pure/logic.ML	Tue Feb 07 19:56:45 2006 +0100
@@ -223,7 +223,7 @@
       | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
 
     val lhs_bads = filter_out check_arg args;
-    val lhs_dups = gen_duplicates (op aconv) args;
+    val lhs_dups = duplicates (op aconv) args;
     val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
       if is_fixed x orelse member (op aconv) args v then I
       else insert (op aconv) v | _ => I) rhs [];

--- a/src/Pure/type.ML	Tue Feb 07 08:47:43 2006 +0100
+++ b/src/Pure/type.ML	Tue Feb 07 19:56:45 2006 +0100
@@ -624,7 +624,7 @@
     val rhs' = strip_sorts (no_tvars (cert_typ_syntax tsig rhs))
       handle TYPE (msg, _, _) => err msg;
   in
-    (case gen_duplicates (op =) vs of
+    (case duplicates (op =) vs of
       [] => []
     | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups));
     (case gen_rems (op =) (map (#1 o #1) (typ_tvars rhs'), vs) of

--- a/src/Pure/type_infer.ML	Tue Feb 07 08:47:43 2006 +0100
+++ b/src/Pure/type_infer.ML	Tue Feb 07 19:56:45 2006 +0100
@@ -462,7 +462,7 @@
       xi = xi' andalso Type.eq_sort tsig (S, S');
 
     val env = gen_distinct eq (map (apsnd map_sort) raw_env);
-    val _ = (case gen_duplicates (eq_fst (op =)) env of [] => ()
+    val _ = (case duplicates (eq_fst (op =)) env of [] => ()
       | dups => error ("Inconsistent sort constraints for type variable(s) "
           ^ commas_quote (map (Syntax.string_of_vname' o fst) dups)));