# HG changeset patch # User wenzelm # Date 1139338605 -3600 # Node ID 67f572e0323695af6c50a67355b310bf7978db33 # Parent 3adfc9dfb30a03ea2a127e651b9948abfa83621a renamed gen_duplicates to duplicates; diff -r 3adfc9dfb30a -r 67f572e03236 src/HOL/Tools/datatype_package.ML --- 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'))], diff -r 3adfc9dfb30a -r 67f572e03236 src/HOL/Tools/inductive_codegen.ML --- 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 diff -r 3adfc9dfb30a -r 67f572e03236 src/HOL/Tools/primrec_package.ML --- 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 diff -r 3adfc9dfb30a -r 67f572e03236 src/HOL/Tools/record_package.ML --- 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]); diff -r 3adfc9dfb30a -r 67f572e03236 src/HOL/Tools/typedef_package.ML --- 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 = diff -r 3adfc9dfb30a -r 67f572e03236 src/HOLCF/domain/extender.ML --- 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, diff -r 3adfc9dfb30a -r 67f572e03236 src/Pure/Isar/locale.ML --- 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) => diff -r 3adfc9dfb30a -r 67f572e03236 src/Pure/Isar/session.ML --- 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; diff -r 3adfc9dfb30a -r 67f572e03236 src/Pure/Syntax/syntax.ML --- 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))) diff -r 3adfc9dfb30a -r 67f572e03236 src/Pure/axclass.ML --- 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; diff -r 3adfc9dfb30a -r 67f572e03236 src/Pure/logic.ML --- 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 []; diff -r 3adfc9dfb30a -r 67f572e03236 src/Pure/type.ML --- 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 diff -r 3adfc9dfb30a -r 67f572e03236 src/Pure/type_infer.ML --- 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)));