--- a/src/HOL/Tools/datatype_package.ML Mon Feb 06 11:00:24 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML Mon Feb 06 11:01:28 2006 +0100
@@ -564,7 +564,7 @@
TYPE (msg, _, _) => error msg;
val sorts' = add_typ_tfrees (T, sorts)
in (Ts @ [T],
- case duplicates (map fst sorts') of
+ case gen_duplicates (op =) (map fst sorts') of
[] => sorts'
| dups => error ("Inconsistent sort constraints for " ^ commas dups))
end;
@@ -956,14 +956,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 duplicates tvs of
+ in (case gen_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 duplicates (map fst new_dts) @ duplicates new_type_names of
+ val _ = (case gen_duplicates (op =) (map fst new_dts) @ gen_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)) =
@@ -986,7 +986,7 @@
Library.foldl prep_constr (([], [], sorts), constrs)
in
- case duplicates (map fst constrs') of
+ case gen_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 Mon Feb 06 11:00:24 2006 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Mon Feb 06 11:01:28 2006 +0100
@@ -229,7 +229,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 (duplicates vTs) @
+ val dupTs = map snd (gen_duplicates (op =) vTs) @
List.mapPartial (AList.lookup (op =) vTs) vs;
in
terms_vs (in_ts @ in_ts') subset vs andalso
@@ -256,7 +256,7 @@
val in_vs = terms_vs in_ts;
val concl_vs = terms_vs ts
in
- forall is_eqT (map snd (duplicates (List.concat (map term_vTs in_ts)))) andalso
+ forall is_eqT (map snd (gen_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 Mon Feb 06 11:00:24 2006 +0100
+++ b/src/HOL/Tools/primrec_package.ML Mon Feb 06 11:01:28 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: " (duplicates lfrees);
+ (check_vars "repeated variable names in pattern: " (gen_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 Mon Feb 06 11:00:24 2006 +0100
+++ b/src/HOL/Tools/record_package.ML Mon Feb 06 11:01:28 2006 +0100
@@ -2060,7 +2060,7 @@
else ["Duplicate definition of record " ^ quote name];
val err_dup_parms =
- (case duplicates params of
+ (case gen_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 duplicates (map #1 bfields) of
+ (case gen_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 duplicates envir_names of
+ (case gen_duplicates (op =) envir_names of
[] => []
| dups => ["Inconsistent sort constraints for " ^ commas dups]);
--- a/src/HOL/Tools/typedef_package.ML Mon Feb 06 11:00:24 2006 +0100
+++ b/src/HOL/Tools/typedef_package.ML Mon Feb 06 11:01:28 2006 +0100
@@ -200,7 +200,7 @@
else ["Illegal schematic variable(s) on rhs"];
val dup_lhs_tfrees =
- (case duplicates lhs_tfrees of [] => []
+ (case gen_duplicates (op =) lhs_tfrees of [] => []
| dups => ["Duplicate type variables on lhs: " ^ show_names dups]);
val extra_rhs_tfrees =
--- a/src/HOLCF/domain/extender.ML Mon Feb 06 11:00:24 2006 +0100
+++ b/src/HOLCF/domain/extender.ML Mon Feb 06 11:01:28 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 duplicates (map fst dtnvs) of
+ val test_dupl_typs = (case gen_duplicates (op =) (map fst dtnvs) of
[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
- val test_dupl_cons = (case duplicates (map first (List.concat cons'')) of
+ val test_dupl_cons = (case gen_duplicates (op =) (map first (List.concat cons'')) of
[] => false | dups => error ("Duplicate constructors: "
^ commas_quote dups));
- val test_dupl_sels = (case duplicates (List.mapPartial second
+ val test_dupl_sels = (case gen_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 duplicates(map(fst o dest_TFree)s)of
+ val test_dupl_tvars = exists(fn s=>case gen_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/proof_context.ML Mon Feb 06 11:00:24 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML Mon Feb 06 11:01:28 2006 +0100
@@ -1115,7 +1115,7 @@
val (ys, zs) = split_list (fixes_of ctxt);
val (vars, ctxt') = prep raw_vars ctxt;
val xs = map #1 vars;
- val _ = no_dups ctxt (duplicates xs);
+ val _ = no_dups ctxt (gen_duplicates (op =) xs);
val xs' =
if is_body ctxt then Term.variantlist (map Syntax.skolem xs, zs)
else (no_dups ctxt (xs inter_string ys); no_dups ctxt (xs inter_string zs); xs);
--- a/src/Pure/Isar/session.ML Mon Feb 06 11:00:24 2006 +0100
+++ b/src/Pure/Isar/session.ML Mon Feb 06 11:01:28 2006 +0100
@@ -41,7 +41,7 @@
fun add_path reset s =
let val sess = ! session @ [s] in
- (case Library.duplicates sess of
+ (case gen_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/Proof/extraction.ML Mon Feb 06 11:00:24 2006 +0100
+++ b/src/Pure/Proof/extraction.ML Mon Feb 06 11:01:28 2006 +0100
@@ -365,7 +365,7 @@
val is_def =
(case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
- (Const _, ts) => forall is_Var ts andalso null (duplicates ts)
+ (Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts)
andalso can (Thm.get_axiom_i thy) name
| _ => false) handle TERM _ => false;
in
--- a/src/Pure/proofterm.ML Mon Feb 06 11:00:24 2006 +0100
+++ b/src/Pure/proofterm.ML Mon Feb 06 11:01:28 2006 +0100
@@ -902,8 +902,8 @@
if ch orelse ch' then prf' % Option.map compress_term t' else prf) end
| shrink' ls lev ts prfs (prf as PBound i) =
(if exists (fn SOME (Bound j) => lev-j <= List.nth (ls, i) | _ => true) ts
- orelse not (null (duplicates
- (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))))
+ orelse has_duplicates (op =)
+ (Library.foldl (fn (js, SOME (Bound j)) => j :: js | (js, _) => js) ([], ts))
orelse exists #1 prfs then [i] else [], false, map (pair false) ts, prf)
| shrink' ls lev ts prfs (Hyp t) = ([], false, map (pair false) ts, Hyp (compress_term t))
| shrink' ls lev ts prfs (prf as MinProof _) =
--- a/src/Pure/sign.ML Mon Feb 06 11:00:24 2006 +0100
+++ b/src/Pure/sign.ML Mon Feb 06 11:01:28 2006 +0100
@@ -628,7 +628,7 @@
fun add_typedecls decls thy =
let
fun type_of (a, vs, mx) =
- if null (duplicates vs) then (a, length vs, mx)
+ if not (has_duplicates (op =) vs) then (a, length vs, mx)
else error ("Duplicate parameters in type declaration: " ^ quote a);
in add_types (map type_of decls) thy end;
--- a/src/Pure/type.ML Mon Feb 06 11:00:24 2006 +0100
+++ b/src/Pure/type.ML Mon Feb 06 11:01:28 2006 +0100
@@ -624,7 +624,7 @@
val rhs' = strip_sorts (no_tvars (cert_typ_syntax tsig rhs))
handle TYPE (msg, _, _) => err msg;
in
- (case duplicates vs of
+ (case gen_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/ZF/Tools/primrec_package.ML Mon Feb 06 11:00:24 2006 +0100
+++ b/src/ZF/Tools/primrec_package.ML Mon Feb 06 11:01:28 2006 +0100
@@ -71,7 +71,7 @@
val new_eqn = (cname, (rhs, cargs, eq))
in
- if not (null (duplicates lfrees)) then
+ if (not o null o gen_duplicates (op =)) lfrees then
raise RecError "repeated variable name in pattern"
else if not ((map dest_Free (term_frees rhs)) subset lfrees) then
raise RecError "extra variables on rhs"