# HG changeset patch # User wenzelm # Date 1140035695 -3600 # Node ID bc5c6c9b114e8036b9c6c665b96a15d887e5c68c # Parent 75786c2eb897d1d7130f1e928dd46a65a2e3f20f removed distinct, renamed gen_distinct to distinct; diff -r 75786c2eb897 -r bc5c6c9b114e TFL/tfl.ML --- 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, diff -r 75786c2eb897 -r bc5c6c9b114e TFL/usyntax.ML --- 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" diff -r 75786c2eb897 -r bc5c6c9b114e src/FOLP/IFOLP.ML --- 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 diff -r 75786c2eb897 -r bc5c6c9b114e src/HOL/Tools/ATP/recon_transfer_proof.ML --- 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 diff -r 75786c2eb897 -r bc5c6c9b114e src/HOL/Tools/datatype_package.ML --- 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] diff -r 75786c2eb897 -r bc5c6c9b114e src/HOL/Tools/inductive_codegen.ML --- 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; diff -r 75786c2eb897 -r bc5c6c9b114e src/HOL/Tools/inductive_realizer.ML --- 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 **) diff -r 75786c2eb897 -r bc5c6c9b114e src/HOL/Tools/meson.ML --- 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 = diff -r 75786c2eb897 -r bc5c6c9b114e src/HOL/Tools/primrec_package.ML --- 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, ...}) => diff -r 75786c2eb897 -r bc5c6c9b114e src/HOL/Tools/record_package.ML --- 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 diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/Isar/attrib.ML --- 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 diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/Isar/context_rules.ML --- 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 *) diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/Isar/find_theorems.ML --- 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 = diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/Isar/induct_attrib.ML --- 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 diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/Isar/method.ML --- 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 *) diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/Isar/rule_cases.ML --- 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; diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/Syntax/parser.ML --- 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)))); diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/Syntax/printer.ML --- 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; diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/Syntax/syn_ext.ML --- 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, diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/Syntax/syntax.ML --- 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 diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/Thy/present.ML --- 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); diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/codegen.ML --- 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) diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/context.ML --- 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" diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/library.ML --- 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*) diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/pure_thy.ML --- 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 = diff -r 75786c2eb897 -r bc5c6c9b114e src/Pure/type_infer.ML --- 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)));