--- a/TFL/tfl.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/TFL/tfl.ML Wed Feb 15 21:34:55 2006 +0100
@@ -316,7 +316,7 @@
| single [f] = f
| single fs =
(*multiple function names?*)
- if length (gen_distinct same_name fs) < length fs
+ if length (distinct same_name fs) < length fs
then mk_functional_err
"The function being declared appears with multiple types"
else mk_functional_err
@@ -328,7 +328,7 @@
handle TERM _ => raise TFL_ERR "mk_functional"
"recursion equations must use the = relation")
val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
- val atom = single (gen_distinct (op aconv) funcs)
+ val atom = single (distinct (op aconv) funcs)
val (fname,ftype) = dest_atom atom
val dummy = map (no_repeat_vars thy) pats
val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
--- a/TFL/usyntax.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/TFL/usyntax.ML Wed Feb 15 21:34:55 2006 +0100
@@ -115,7 +115,7 @@
val is_vartype = can dest_vtype;
val type_vars = map mk_prim_vartype o typ_tvars
-fun type_varsl L = distinct (fold (curry op @ o type_vars) L []);
+fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []);
val alpha = mk_vartype "'a"
val beta = mk_vartype "'b"
--- a/src/FOLP/IFOLP.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/FOLP/IFOLP.ML Wed Feb 15 21:34:55 2006 +0100
@@ -77,7 +77,7 @@
and concl = discard_proof (Logic.strip_assums_concl prem)
in
if exists (fn hyp => hyp aconv concl) hyps
- then case gen_distinct (op =) (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of
+ then case distinct (op =) (filter (fn hyp => could_unify (hyp, concl)) hyps) of
[_] => assume_tac i
| _ => no_tac
else no_tac
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Wed Feb 15 21:34:55 2006 +0100
@@ -158,9 +158,8 @@
(* get names of clasimp axioms used*)
fun get_axiom_names step_nums clause_arr =
- distinct (sort_strings
- (map (ResClause.get_axiomName o #1)
- (get_clasimp_cls clause_arr step_nums)));
+ sort_distinct string_ord
+ (map (ResClause.get_axiomName o #1) (get_clasimp_cls clause_arr step_nums));
(*String contains multiple lines. We want those of the form
"253[0:Inp] et cetera..."
@@ -221,13 +220,13 @@
val vars = map thm_vars clauses
- val distvars = distinct (fold append vars [])
+ val distvars = distinct (op =) (fold append vars [])
val clause_terms = map prop_of clauses
val clause_frees = List.concat (map term_frees clause_terms)
val frees = map lit_string_with_nums clause_frees;
- val distfrees = distinct frees
+ val distfrees = distinct (op =) frees
val metas = map Meson.make_meta_clause clauses
val ax_strs = map #3 axioms
--- a/src/HOL/Tools/datatype_package.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML Wed Feb 15 21:34:55 2006 +0100
@@ -326,7 +326,7 @@
fun dt_cases (descr: descr) (_, args, constrs) =
let
fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
- val bnames = map the_bname (distinct (List.concat (map dt_recs args)));
+ val bnames = map the_bname (distinct (op =) (List.concat (map dt_recs args)));
in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
@@ -492,7 +492,7 @@
([], true, SOME _) =>
case_error "Extra '_' dummy pattern" (SOME tname) [u]
| (_ :: _, _, _) =>
- let val extra = distinct (map (fst o fst) cases'')
+ let val extra = distinct (op =) (map (fst o fst) cases'')
in case extra \\ map fst constrs of
[] => case_error ("More than one clause for constructor(s) " ^
commas extra) (SOME tname) [u]
--- a/src/HOL/Tools/inductive_codegen.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Wed Feb 15 21:34:55 2006 +0100
@@ -177,7 +177,7 @@
string_of_mode ms)) modes));
val term_vs = map (fst o fst o dest_Var) o term_vars;
-val terms_vs = distinct o List.concat o (map term_vs);
+val terms_vs = distinct (op =) o List.concat o (map term_vs);
(** collect all Vars in a term (with duplicates!) **)
fun term_vTs tm =
@@ -441,7 +441,7 @@
end
| compile_prems out_ts vs names gr ps =
let
- val vs' = distinct (List.concat (vs :: map term_vs out_ts));
+ val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts));
val SOME (p, mode as SOME (Mode ((_, js), _))) =
select_mode_prem thy modes' vs' ps;
val ps' = filter_out (equal p) ps;
--- a/src/HOL/Tools/inductive_realizer.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Wed Feb 15 21:34:55 2006 +0100
@@ -324,7 +324,7 @@
||> Extraction.add_typeof_eqns_i ty_eqs
||> Extraction.add_realizes_eqns_i rlz_eqs;
fun get f = (these oo Option.map) f;
- val rec_names = distinct (map (fst o dest_Const o head_of o fst o
+ val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) =>
if s mem rsets then
@@ -341,7 +341,7 @@
c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var)
(rev (Term.add_vars (prop_of intr) []) \\ params')) intr))))
(intrs ~~ List.concat constrss);
- val rlzsets = distinct (map (fn rintr => snd (HOLogic.dest_mem
+ val rlzsets = distinct (op =) (map (fn rintr => snd (HOLogic.dest_mem
(HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)))) rintrs);
(** realizability predicate **)
--- a/src/HOL/Tools/meson.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/HOL/Tools/meson.ML Wed Feb 15 21:34:55 2006 +0100
@@ -420,7 +420,7 @@
(*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
fun make_horns ths =
name_thms "Horn#"
- (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
+ (distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
(*Could simply use nprems_of, which would count remaining subgoals -- no
discrimination as to their size! With BEST_FIRST, fails for problem 41.*)
@@ -525,7 +525,7 @@
fun make_meta_clauses ths =
name_thms "MClause#"
- (gen_distinct Drule.eq_thm_prop (map make_meta_clause ths));
+ (distinct Drule.eq_thm_prop (map make_meta_clause ths));
(*Permute a rule's premises to move the i-th premise to the last position.*)
fun make_last i th =
--- a/src/HOL/Tools/primrec_package.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/HOL/Tools/primrec_package.ML Wed Feb 15 21:34:55 2006 +0100
@@ -227,7 +227,7 @@
val sg = Theory.sign_of thy;
val dt_info = DatatypePackage.get_datatypes thy;
val rec_eqns = foldr (process_eqn sg) [] (map snd eqns);
- val tnames = distinct (map (#1 o snd) rec_eqns);
+ val tnames = distinct (op =) (map (#1 o snd) rec_eqns);
val dts = find_dts dt_info tnames tnames;
val main_fns =
map (fn (tname, {index, ...}) =>
--- a/src/HOL/Tools/record_package.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/HOL/Tools/record_package.ML Wed Feb 15 21:34:55 2006 +0100
@@ -1665,7 +1665,8 @@
(* prepare print translation functions *)
val field_tr's =
- print_translation (distinct (List.concat (map NameSpace.accesses' (full_moreN :: names))));
+ print_translation (distinct (op =)
+ (List.concat (map NameSpace.accesses' (full_moreN :: names))));
val adv_ext_tr's =
let
--- a/src/Pure/Isar/attrib.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/Isar/attrib.ML Wed Feb 15 21:34:55 2006 +0100
@@ -238,8 +238,8 @@
fun prepT (a, T) = (Thm.ctyp_of thy (TVar (a, the_sort sorts a)), Thm.ctyp_of thy T);
fun prep (xi, t) = pairself (Thm.cterm_of thy) (Var (xi, Term.fastype_of t), t);
in
- Drule.instantiate (map prepT (gen_distinct (op =) envT),
- map prep (gen_distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) thm
+ Drule.instantiate (map prepT (distinct (op =) envT),
+ map prep (distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) thm
end;
in
--- a/src/Pure/Isar/context_rules.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/Isar/context_rules.ML Wed Feb 15 21:34:55 2006 +0100
@@ -59,7 +59,7 @@
(elim_queryK, "extra elimination rules (elim?)")];
val rule_kinds = map #1 kind_names;
-val rule_indexes = gen_distinct (op =) (map #1 rule_kinds);
+val rule_indexes = distinct (op =) (map #1 rule_kinds);
(* context data *)
--- a/src/Pure/Isar/find_theorems.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/Isar/find_theorems.ML Wed Feb 15 21:34:55 2006 +0100
@@ -242,7 +242,7 @@
(ProofContext.lthms_containing ctxt spec
|> map PureThy.selections
|> List.concat
- |> gen_distinct (fn ((r1, th1), (r2, th2)) =>
+ |> distinct (fn ((r1, th1), (r2, th2)) =>
r1 = r2 andalso Drule.eq_thm_prop (th1, th2)));
fun print_theorems ctxt opt_goal opt_limit raw_criteria =
--- a/src/Pure/Isar/induct_attrib.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/Isar/induct_attrib.ML Wed Feb 15 21:34:55 2006 +0100
@@ -54,9 +54,7 @@
(* variables -- ordered left-to-right, preferring right *)
fun vars_of tm =
- Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []
- |> gen_distinct (op =)
- |> rev;
+ rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
local
--- a/src/Pure/Isar/method.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/Isar/method.ML Wed Feb 15 21:34:55 2006 +0100
@@ -290,7 +290,7 @@
val remdups_tac = SUBGOAL (fn (g, i) =>
let val prems = Logic.strip_assums_hyp g in
- REPEAT_DETERM_N (length prems - length (gen_distinct op aconv prems))
+ REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
(Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
end);
@@ -393,7 +393,7 @@
map
(fn (xi, t) =>
pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
- (gen_distinct
+ (distinct
(fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
(xis ~~ ts));
(* Lift and instantiate rule *)
--- a/src/Pure/Isar/rule_cases.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/Isar/rule_cases.ML Wed Feb 15 21:34:55 2006 +0100
@@ -130,7 +130,7 @@
in
if len = 0 then NONE
else if len = 1 then SOME (common_case (hd cases))
- else if is_none case_outline orelse length (gen_distinct (op =) (map fst cases)) > 1 then NONE
+ else if is_none case_outline orelse length (distinct (op =) (map fst cases)) > 1 then NONE
else SOME (nested_case (hd cases))
end;
--- a/src/Pure/Syntax/parser.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/Syntax/parser.ML Wed Feb 15 21:34:55 2006 +0100
@@ -845,7 +845,7 @@
SOME (a, prec) | _ => NONE)
(Array.sub (stateset, i-1));
val allowed =
- gen_distinct (op =) (get_starts nts [] @
+ distinct (op =) (get_starts nts [] @
(List.mapPartial (fn (_, _, _, Terminal a :: _, _, _) => SOME a
| _ => NONE)
(Array.sub (stateset, i-1))));
--- a/src/Pure/Syntax/printer.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/Syntax/printer.ML Wed Feb 15 21:34:55 2006 +0100
@@ -253,7 +253,7 @@
fun merge_prtabs prtabs1 prtabs2 =
let
- val modes = gen_distinct (op =) (map fst (prtabs1 @ prtabs2));
+ val modes = distinct (op =) (map fst (prtabs1 @ prtabs2));
fun merge m = (m, Symtab.merge_list (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m));
in map merge modes end;
--- a/src/Pure/Syntax/syn_ext.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/Syntax/syn_ext.ML Wed Feb 15 21:34:55 2006 +0100
@@ -361,12 +361,13 @@
val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
|> split_list |> apsnd (rev o List.concat);
- val mfix_consts = gen_distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
+ val mfix_consts =
+ distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
in
SynExt {
xprods = xprods,
consts = consts union_string mfix_consts,
- prmodes = gen_distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
+ prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
parse_ast_translation = parse_ast_translation,
parse_rules = parse_rules' @ parse_rules,
parse_translation = parse_translation,
--- a/src/Pure/Syntax/syntax.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML Wed Feb 15 21:34:55 2006 +0100
@@ -111,7 +111,7 @@
(** tables of token translation functions **)
fun lookup_tokentr tabs modes =
- let val trs = gen_distinct (eq_fst (op =))
+ let val trs = distinct (eq_fst (op =))
(List.concat (map (these o AList.lookup (op =) tabs) (modes @ [""])))
in fn c => Option.map fst (AList.lookup (op =) trs c) end;
@@ -125,16 +125,14 @@
let
val trs1 = these (AList.lookup (op =) tabs1 mode);
val trs2 = these (AList.lookup (op =) tabs2 mode);
- val trs = gen_distinct eq_tr (trs1 @ trs2);
+ val trs = distinct eq_tr (trs1 @ trs2);
in
(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)))
end;
- in
- map merge (gen_distinct (op =) (map fst (tabs1 @ tabs2)))
- end;
+ in map merge (distinct (op =) (map fst (tabs1 @ tabs2))) end;
fun extend_tokentrtab tokentrs tabs =
let
--- a/src/Pure/Thy/present.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/Thy/present.ML Wed Feb 15 21:34:55 2006 +0100
@@ -273,7 +273,7 @@
| _ => error ("Malformed document version specification: " ^ quote str));
fun read_versions strs =
- rev (gen_distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
+ rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
|> filter_out (equal "-" o #2);
--- a/src/Pure/codegen.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/codegen.ML Wed Feb 15 21:34:55 2006 +0100
@@ -856,7 +856,7 @@
in
if module = "" then
let
- val modules = gen_distinct (op =) (map (#2 o snd) code);
+ val modules = distinct (op =) (map (#2 o snd) code);
val mod_gr = foldr (uncurry Graph.add_edge_acyclic)
(foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules)
(List.concat (map (fn (s, (_, module, _)) => map (pair module)
--- a/src/Pure/context.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/context.ML Wed Feb 15 21:34:55 2006 +0100
@@ -379,8 +379,8 @@
else
let
val parents =
- maximal_thys (gen_distinct eq_thy (map check_thy imports));
- val ancestors = gen_distinct eq_thy (parents @ List.concat (map ancestors_of parents));
+ maximal_thys (distinct eq_thy (map check_thy imports));
+ val ancestors = distinct eq_thy (parents @ List.concat (map ancestors_of parents));
val Theory ({id, ids, iids, ...}, data, _, _) =
(case parents of
[] => error "No parent theories"
--- a/src/Pure/library.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/library.ML Wed Feb 15 21:34:55 2006 +0100
@@ -214,9 +214,8 @@
val \\ : ''a list * ''a list -> ''a list
val gen_rem: ('a * 'b -> bool) -> 'a list * 'b -> 'a list
val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
- val gen_distinct: ('a * 'a -> bool) -> 'a list -> 'a list
- val distinct: ''a list -> ''a list
val findrep: ''a list -> ''a list
+ val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
@@ -1011,24 +1010,20 @@
fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
fun gen_rems eq (xs, ys) = filter_out (member eq ys) xs;
+(*returns the tail beginning with the first repeated element, or []*)
+fun findrep [] = []
+ | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
+
+
(*makes a list of the distinct members of the input; preserves order, takes
first of equal elements*)
-fun gen_distinct eq lst =
+fun distinct eq lst =
let
fun dist (rev_seen, []) = rev rev_seen
| dist (rev_seen, x :: xs) =
if member eq rev_seen x then dist (rev_seen, xs)
else dist (x :: rev_seen, xs);
- in
- dist ([], lst)
- end;
-
-fun distinct l = gen_distinct (op =) l;
-
-(*returns the tail beginning with the first repeated element, or []*)
-fun findrep [] = []
- | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
-
+ in dist ([], lst) end;
(*returns a list containing all repeated elements exactly once; preserves
order, takes first of equal elements*)
--- a/src/Pure/pure_thy.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/pure_thy.ML Wed Feb 15 21:34:55 2006 +0100
@@ -312,7 +312,7 @@
|> map (fn thy =>
FactIndex.find (fact_index_of thy) spec
|> List.filter (fn (name, ths) => valid_thms theory (Name name, ths))
- |> gen_distinct (eq_fst (op =)))
+ |> distinct (eq_fst (op =)))
|> List.concat;
fun thms_containing_consts thy consts =
--- a/src/Pure/type_infer.ML Wed Feb 15 19:11:10 2006 +0100
+++ b/src/Pure/type_infer.ML Wed Feb 15 21:34:55 2006 +0100
@@ -461,7 +461,7 @@
fun eq ((xi: indexname, S), (xi', S')) =
xi = xi' andalso Type.eq_sort tsig (S, S');
- val env = gen_distinct eq (map (apsnd map_sort) raw_env);
+ val env = distinct eq (map (apsnd map_sort) raw_env);
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)));