subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
authorhaftmann
Mon Feb 06 11:01:28 2006 +0100 (2006-02-06)
changeset 18928042608ffa2ec
parent 18927 2e5b0f3f1418
child 18929 d81435108688
subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
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/proof_context.ML
src/Pure/Isar/session.ML
src/Pure/Proof/extraction.ML
src/Pure/proofterm.ML
src/Pure/sign.ML
src/Pure/type.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Feb 06 11:00:24 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Feb 06 11:01:28 2006 +0100
     1.3 @@ -564,7 +564,7 @@
     1.4        TYPE (msg, _, _) => error msg;
     1.5      val sorts' = add_typ_tfrees (T, sorts)
     1.6    in (Ts @ [T],
     1.7 -      case duplicates (map fst sorts') of
     1.8 +      case gen_duplicates (op =) (map fst sorts') of
     1.9           [] => sorts'
    1.10         | dups => error ("Inconsistent sort constraints for " ^ commas dups))
    1.11    end;
    1.12 @@ -956,14 +956,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 duplicates tvs of
    1.17 +      in (case gen_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 duplicates (map fst new_dts) @ duplicates new_type_names of
    1.25 +    val _ = (case gen_duplicates (op =) (map fst new_dts) @ gen_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 @@ -986,7 +986,7 @@
    1.30            Library.foldl prep_constr (([], [], sorts), constrs)
    1.31  
    1.32        in
    1.33 -        case duplicates (map fst constrs') of
    1.34 +        case gen_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	Mon Feb 06 11:00:24 2006 +0100
     2.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Mon Feb 06 11:01:28 2006 +0100
     2.3 @@ -229,7 +229,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 (duplicates vTs) @
     2.8 +            val dupTs = map snd (gen_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 @@ -256,7 +256,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 (duplicates (List.concat (map term_vTs in_ts)))) andalso
    2.17 +    forall is_eqT (map snd (gen_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	Mon Feb 06 11:00:24 2006 +0100
     3.2 +++ b/src/HOL/Tools/primrec_package.ML	Mon Feb 06 11:01:28 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: " (duplicates lfrees);
     3.8 +     (check_vars "repeated variable names in pattern: " (gen_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	Mon Feb 06 11:00:24 2006 +0100
     4.2 +++ b/src/HOL/Tools/record_package.ML	Mon Feb 06 11:01:28 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 duplicates params of
     4.8 +      (case gen_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 duplicates (map #1 bfields) of
    4.17 +      (case gen_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 duplicates envir_names of
    4.26 +      (case gen_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	Mon Feb 06 11:00:24 2006 +0100
     5.2 +++ b/src/HOL/Tools/typedef_package.ML	Mon Feb 06 11:01:28 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 duplicates lhs_tfrees of [] => []
     5.8 +      (case gen_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	Mon Feb 06 11:00:24 2006 +0100
     6.2 +++ b/src/HOLCF/domain/extender.ML	Mon Feb 06 11:01:28 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 duplicates (map fst dtnvs) of 
     6.8 +    val test_dupl_typs = (case gen_duplicates (op =) (map fst dtnvs) of 
     6.9  	[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
    6.10 -    val test_dupl_cons = (case duplicates (map first (List.concat cons'')) of 
    6.11 +    val test_dupl_cons = (case gen_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 duplicates (List.mapPartial second
    6.15 +    val test_dupl_sels = (case gen_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 duplicates(map(fst o dest_TFree)s)of
    6.19 +    val test_dupl_tvars = exists(fn s=>case gen_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/proof_context.ML	Mon Feb 06 11:00:24 2006 +0100
     7.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Feb 06 11:01:28 2006 +0100
     7.3 @@ -1115,7 +1115,7 @@
     7.4      val (ys, zs) = split_list (fixes_of ctxt);
     7.5      val (vars, ctxt') = prep raw_vars ctxt;
     7.6      val xs = map #1 vars;
     7.7 -    val _ = no_dups ctxt (duplicates xs);
     7.8 +    val _ = no_dups ctxt (gen_duplicates (op =) xs);
     7.9      val xs' =
    7.10        if is_body ctxt then Term.variantlist (map Syntax.skolem xs, zs)
    7.11        else (no_dups ctxt (xs inter_string ys); no_dups ctxt (xs inter_string zs); xs);
     8.1 --- a/src/Pure/Isar/session.ML	Mon Feb 06 11:00:24 2006 +0100
     8.2 +++ b/src/Pure/Isar/session.ML	Mon Feb 06 11:01:28 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 Library.duplicates sess of
     8.8 +    (case gen_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/Proof/extraction.ML	Mon Feb 06 11:00:24 2006 +0100
     9.2 +++ b/src/Pure/Proof/extraction.ML	Mon Feb 06 11:01:28 2006 +0100
     9.3 @@ -365,7 +365,7 @@
     9.4  
     9.5      val is_def =
     9.6        (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
     9.7 -         (Const _, ts) => forall is_Var ts andalso null (duplicates ts)
     9.8 +         (Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts)
     9.9             andalso can (Thm.get_axiom_i thy) name
    9.10         | _ => false) handle TERM _ => false;
    9.11    in
    10.1 --- a/src/Pure/proofterm.ML	Mon Feb 06 11:00:24 2006 +0100
    10.2 +++ b/src/Pure/proofterm.ML	Mon Feb 06 11:01:28 2006 +0100
    10.3 @@ -902,8 +902,8 @@
    10.4                if ch orelse ch' then prf' % Option.map compress_term t' else prf) end
    10.5        | shrink' ls lev ts prfs (prf as PBound i) =
    10.6            (if exists (fn SOME (Bound j) => lev-j <= List.nth (ls, i) | _ => true) ts
    10.7 -             orelse not (null (duplicates
    10.8 -               (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))))
    10.9 +             orelse has_duplicates (op =)
   10.10 +               (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))
   10.11               orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
   10.12        | shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp (compress_term t))
   10.13        | shrink' ls lev ts prfs (prf as MinProof _) =
    11.1 --- a/src/Pure/sign.ML	Mon Feb 06 11:00:24 2006 +0100
    11.2 +++ b/src/Pure/sign.ML	Mon Feb 06 11:01:28 2006 +0100
    11.3 @@ -628,7 +628,7 @@
    11.4  fun add_typedecls decls thy =
    11.5    let
    11.6      fun type_of (a, vs, mx) =
    11.7 -      if null (duplicates vs) then (a, length vs, mx)
    11.8 +      if not (has_duplicates (op =) vs) then (a, length vs, mx)
    11.9        else error ("Duplicate parameters in type declaration: " ^ quote a);
   11.10    in add_types (map type_of decls) thy end;
   11.11  
    12.1 --- a/src/Pure/type.ML	Mon Feb 06 11:00:24 2006 +0100
    12.2 +++ b/src/Pure/type.ML	Mon Feb 06 11:01:28 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 duplicates vs of
    12.8 +    (case gen_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/ZF/Tools/primrec_package.ML	Mon Feb 06 11:00:24 2006 +0100
    13.2 +++ b/src/ZF/Tools/primrec_package.ML	Mon Feb 06 11:01:28 2006 +0100
    13.3 @@ -71,7 +71,7 @@
    13.4      val new_eqn = (cname, (rhs, cargs, eq))
    13.5  
    13.6    in
    13.7 -    if not (null (duplicates lfrees)) then
    13.8 +    if (not o null o gen_duplicates (op =)) lfrees then
    13.9        raise RecError "repeated variable name in pattern"
   13.10      else if not ((map dest_Free (term_frees rhs)) subset lfrees) then
   13.11        raise RecError "extra variables on rhs"