renamed gen_duplicates to duplicates;
authorwenzelm
Tue Feb 07 19:56:45 2006 +0100 (2006-02-07)
changeset 1896467f572e03236
parent 18963 3adfc9dfb30a
child 18965 3b76383e3ab3
renamed gen_duplicates to duplicates;
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/typedef_package.ML
src/HOLCF/domain/extender.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/session.ML
src/Pure/Syntax/syntax.ML
src/Pure/axclass.ML
src/Pure/logic.ML
src/Pure/type.ML
src/Pure/type_infer.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Feb 07 08:47:43 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Feb 07 19:56:45 2006 +0100
     1.3 @@ -540,7 +540,7 @@
     1.4        TYPE (msg, _, _) => error msg;
     1.5      val sorts' = add_typ_tfrees (T, sorts)
     1.6    in (Ts @ [T],
     1.7 -      case gen_duplicates (op =) (map fst sorts') of
     1.8 +      case duplicates (op =) (map fst sorts') of
     1.9           [] => sorts'
    1.10         | dups => error ("Inconsistent sort constraints for " ^ commas dups))
    1.11    end;
    1.12 @@ -932,14 +932,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 gen_duplicates (op =) tvs of
    1.17 +      in (case 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 gen_duplicates (op =) (map fst new_dts) @ gen_duplicates (op =) new_type_names of
    1.25 +    val _ = (case duplicates (op =) (map fst new_dts) @ 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 @@ -962,7 +962,7 @@
    1.30            Library.foldl prep_constr (([], [], sorts), constrs)
    1.31  
    1.32        in
    1.33 -        case gen_duplicates (op =) (map fst constrs') of
    1.34 +        case 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'))],
     2.1 --- a/src/HOL/Tools/inductive_codegen.ML	Tue Feb 07 08:47:43 2006 +0100
     2.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Tue Feb 07 19:56:45 2006 +0100
     2.3 @@ -231,7 +231,7 @@
     2.4              val (in_ts, out_ts) = get_args is 1 us;
     2.5              val (out_ts', in_ts') = List.partition (is_constrt thy) out_ts;
     2.6              val vTs = List.concat (map term_vTs out_ts');
     2.7 -            val dupTs = map snd (gen_duplicates (op =) vTs) @
     2.8 +            val dupTs = map snd (duplicates (op =) vTs) @
     2.9                List.mapPartial (AList.lookup (op =) vTs) vs;
    2.10            in
    2.11              terms_vs (in_ts @ in_ts') subset vs andalso
    2.12 @@ -258,7 +258,7 @@
    2.13      val in_vs = terms_vs in_ts;
    2.14      val concl_vs = terms_vs ts
    2.15    in
    2.16 -    forall is_eqT (map snd (gen_duplicates (op =) (List.concat (map term_vTs in_ts)))) andalso
    2.17 +    forall is_eqT (map snd (duplicates (op =) (List.concat (map term_vTs in_ts)))) andalso
    2.18      forall (is_eqT o fastype_of) in_ts' andalso
    2.19      (case check_mode_prems (arg_vs union in_vs) ps of
    2.20         NONE => false
     3.1 --- a/src/HOL/Tools/primrec_package.ML	Tue Feb 07 08:47:43 2006 +0100
     3.2 +++ b/src/HOL/Tools/primrec_package.ML	Tue Feb 07 19:56:45 2006 +0100
     3.3 @@ -69,7 +69,7 @@
     3.4      if length middle > 1 then 
     3.5        raise RecError "more than one non-variable in pattern"
     3.6      else
     3.7 -     (check_vars "repeated variable names in pattern: " (gen_duplicates (op =) lfrees);
     3.8 +     (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
     3.9        check_vars "extra variables on rhs: "
    3.10          (map dest_Free (term_frees rhs) \\ lfrees);
    3.11        case AList.lookup (op =) rec_fns fnameT of
     4.1 --- a/src/HOL/Tools/record_package.ML	Tue Feb 07 08:47:43 2006 +0100
     4.2 +++ b/src/HOL/Tools/record_package.ML	Tue Feb 07 19:56:45 2006 +0100
     4.3 @@ -2060,7 +2060,7 @@
     4.4        else ["Duplicate definition of record " ^ quote name];
     4.5  
     4.6      val err_dup_parms =
     4.7 -      (case gen_duplicates (op =) params of
     4.8 +      (case duplicates (op =) params of
     4.9          [] => []
    4.10        | dups => ["Duplicate parameter(s) " ^ commas dups]);
    4.11  
    4.12 @@ -2072,7 +2072,7 @@
    4.13      val err_no_fields = if null bfields then ["No fields present"] else [];
    4.14  
    4.15      val err_dup_fields =
    4.16 -      (case gen_duplicates (op =) (map #1 bfields) of
    4.17 +      (case duplicates (op =) (map #1 bfields) of
    4.18          [] => []
    4.19        | dups => ["Duplicate field(s) " ^ commas_quote dups]);
    4.20  
    4.21 @@ -2081,7 +2081,7 @@
    4.22        else ["Illegal field name " ^ quote moreN];
    4.23  
    4.24      val err_dup_sorts =
    4.25 -      (case gen_duplicates (op =) envir_names of
    4.26 +      (case duplicates (op =) envir_names of
    4.27          [] => []
    4.28        | dups => ["Inconsistent sort constraints for " ^ commas dups]);
    4.29  
     5.1 --- a/src/HOL/Tools/typedef_package.ML	Tue Feb 07 08:47:43 2006 +0100
     5.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue Feb 07 19:56:45 2006 +0100
     5.3 @@ -200,7 +200,7 @@
     5.4        else ["Illegal schematic variable(s) on rhs"];
     5.5  
     5.6      val dup_lhs_tfrees =
     5.7 -      (case gen_duplicates (op =) lhs_tfrees of [] => []
     5.8 +      (case duplicates (op =) lhs_tfrees of [] => []
     5.9        | dups => ["Duplicate type variables on lhs: " ^ show_names dups]);
    5.10  
    5.11      val extra_rhs_tfrees =
     6.1 --- a/src/HOLCF/domain/extender.ML	Tue Feb 07 08:47:43 2006 +0100
     6.2 +++ b/src/HOLCF/domain/extender.ML	Tue Feb 07 19:56:45 2006 +0100
     6.3 @@ -43,15 +43,15 @@
     6.4       cons'' : ((string * mixfix * (bool * string option * typ) list) list) list) sg =
     6.5    let
     6.6      val defaultS = Sign.defaultS sg;
     6.7 -    val test_dupl_typs = (case gen_duplicates (op =) (map fst dtnvs) of 
     6.8 +    val test_dupl_typs = (case duplicates (op =) (map fst dtnvs) of 
     6.9  	[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
    6.10 -    val test_dupl_cons = (case gen_duplicates (op =) (map first (List.concat cons'')) of 
    6.11 +    val test_dupl_cons = (case duplicates (op =) (map first (List.concat cons'')) of 
    6.12  	[] => false | dups => error ("Duplicate constructors: " 
    6.13  							 ^ commas_quote dups));
    6.14 -    val test_dupl_sels = (case gen_duplicates (op =) (List.mapPartial second
    6.15 +    val test_dupl_sels = (case duplicates (op =) (List.mapPartial second
    6.16  			       (List.concat (map third (List.concat cons'')))) of
    6.17          [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
    6.18 -    val test_dupl_tvars = exists(fn s=>case gen_duplicates (op =) (map(fst o dest_TFree)s)of
    6.19 +    val test_dupl_tvars = exists(fn s=>case duplicates (op =) (map(fst o dest_TFree)s)of
    6.20  	[] => false | dups => error("Duplicate type arguments: " 
    6.21  		   ^commas_quote dups)) (map snd dtnvs);
    6.22      (* test for free type variables, illegal sort constraints on rhs,
     7.1 --- a/src/Pure/Isar/locale.ML	Tue Feb 07 08:47:43 2006 +0100
     7.2 +++ b/src/Pure/Isar/locale.ML	Tue Feb 07 19:56:45 2006 +0100
     7.3 @@ -675,7 +675,7 @@
     7.4  
     7.5      fun rename_parms top ren ((name, ps), (parms, mode)) =
     7.6        let val ps' = map (Element.rename ren) ps in
     7.7 -        (case duplicates ps' of
     7.8 +        (case duplicates (op =) ps' of
     7.9            [] => ((name, ps'),
    7.10                   if top then (map (Element.rename ren) parms,
    7.11                     map_mode (map (fn (t, th) =>
     8.1 --- a/src/Pure/Isar/session.ML	Tue Feb 07 08:47:43 2006 +0100
     8.2 +++ b/src/Pure/Isar/session.ML	Tue Feb 07 19:56:45 2006 +0100
     8.3 @@ -41,7 +41,7 @@
     8.4  
     8.5  fun add_path reset s =
     8.6    let val sess = ! session @ [s] in
     8.7 -    (case gen_duplicates (op =) sess of
     8.8 +    (case duplicates (op =) sess of
     8.9        [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
    8.10      | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
    8.11    end;
     9.1 --- a/src/Pure/Syntax/syntax.ML	Tue Feb 07 08:47:43 2006 +0100
     9.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Feb 07 19:56:45 2006 +0100
     9.3 @@ -127,7 +127,7 @@
     9.4          val trs2 = these (AList.lookup (op =) tabs2 mode);
     9.5          val trs = gen_distinct eq_tr (trs1 @ trs2);
     9.6        in
     9.7 -        (case gen_duplicates (eq_fst (op =)) trs of
     9.8 +        (case duplicates (eq_fst (op =)) trs of
     9.9            [] => (mode, trs)
    9.10          | dups => error ("More than one token translation function in mode " ^
    9.11              quote mode ^ " for " ^ commas_quote (map name dups)))
    10.1 --- a/src/Pure/axclass.ML	Tue Feb 07 08:47:43 2006 +0100
    10.2 +++ b/src/Pure/axclass.ML	Tue Feb 07 19:56:45 2006 +0100
    10.3 @@ -99,7 +99,7 @@
    10.4          Type (t, tys) => (t, map dest_varT tys handle TYPE _ => err ())
    10.5        | _ => err ());
    10.6      val ss =
    10.7 -      if null (gen_duplicates (eq_fst (op =)) tvars)
    10.8 +      if null (duplicates (eq_fst (op =)) tvars)
    10.9        then map snd tvars else err ();
   10.10    in (t, ss, c) end;
   10.11  
    11.1 --- a/src/Pure/logic.ML	Tue Feb 07 08:47:43 2006 +0100
    11.2 +++ b/src/Pure/logic.ML	Tue Feb 07 19:56:45 2006 +0100
    11.3 @@ -223,7 +223,7 @@
    11.4        | close_arg x t = Term.all (Term.fastype_of x) $ lambda x t;
    11.5  
    11.6      val lhs_bads = filter_out check_arg args;
    11.7 -    val lhs_dups = gen_duplicates (op aconv) args;
    11.8 +    val lhs_dups = duplicates (op aconv) args;
    11.9      val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
   11.10        if is_fixed x orelse member (op aconv) args v then I
   11.11        else insert (op aconv) v | _ => I) rhs [];
    12.1 --- a/src/Pure/type.ML	Tue Feb 07 08:47:43 2006 +0100
    12.2 +++ b/src/Pure/type.ML	Tue Feb 07 19:56:45 2006 +0100
    12.3 @@ -624,7 +624,7 @@
    12.4      val rhs' = strip_sorts (no_tvars (cert_typ_syntax tsig rhs))
    12.5        handle TYPE (msg, _, _) => err msg;
    12.6    in
    12.7 -    (case gen_duplicates (op =) vs of
    12.8 +    (case duplicates (op =) vs of
    12.9        [] => []
   12.10      | dups => err ("Duplicate variables on lhs: " ^ commas_quote dups));
   12.11      (case gen_rems (op =) (map (#1 o #1) (typ_tvars rhs'), vs) of
    13.1 --- a/src/Pure/type_infer.ML	Tue Feb 07 08:47:43 2006 +0100
    13.2 +++ b/src/Pure/type_infer.ML	Tue Feb 07 19:56:45 2006 +0100
    13.3 @@ -462,7 +462,7 @@
    13.4        xi = xi' andalso Type.eq_sort tsig (S, S');
    13.5  
    13.6      val env = gen_distinct eq (map (apsnd map_sort) raw_env);
    13.7 -    val _ = (case gen_duplicates (eq_fst (op =)) env of [] => ()
    13.8 +    val _ = (case duplicates (eq_fst (op =)) env of [] => ()
    13.9        | dups => error ("Inconsistent sort constraints for type variable(s) "
   13.10            ^ commas_quote (map (Syntax.string_of_vname' o fst) dups)));
   13.11