# HG changeset patch # User haftmann # Date 1139405940 -3600 # Node ID f24c416a48146f38a50776e443a2a2831bf6a099 # Parent 4efb82669880c8d709063cedf693cdfac28f1464 introduced gen_distinct in place of distinct diff -r 4efb82669880 -r f24c416a4814 src/FOLP/IFOLP.ML --- a/src/FOLP/IFOLP.ML Wed Feb 08 09:27:20 2006 +0100 +++ b/src/FOLP/IFOLP.ML Wed Feb 08 14:39:00 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 distinct (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of + then case gen_distinct (op =) (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of [_] => assume_tac i | _ => no_tac else no_tac diff -r 4efb82669880 -r f24c416a4814 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Wed Feb 08 09:27:20 2006 +0100 +++ b/src/Pure/Isar/attrib.ML Wed Feb 08 14:39:00 2006 +0100 @@ -253,7 +253,7 @@ 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 (distinct envT), + 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 end; diff -r 4efb82669880 -r f24c416a4814 src/Pure/Isar/context_rules.ML --- a/src/Pure/Isar/context_rules.ML Wed Feb 08 09:27:20 2006 +0100 +++ b/src/Pure/Isar/context_rules.ML Wed Feb 08 14:39:00 2006 +0100 @@ -59,7 +59,7 @@ (elim_queryK, "extra elimination rules (elim?)")]; val rule_kinds = map #1 kind_names; -val rule_indexes = distinct (map #1 rule_kinds); +val rule_indexes = gen_distinct (op =) (map #1 rule_kinds); (* context data *) diff -r 4efb82669880 -r f24c416a4814 src/Pure/Isar/induct_attrib.ML --- a/src/Pure/Isar/induct_attrib.ML Wed Feb 08 09:27:20 2006 +0100 +++ b/src/Pure/Isar/induct_attrib.ML Wed Feb 08 14:39:00 2006 +0100 @@ -55,7 +55,7 @@ fun vars_of tm = Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm [] - |> Library.distinct + |> gen_distinct (op =) |> rev; local diff -r 4efb82669880 -r f24c416a4814 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Wed Feb 08 09:27:20 2006 +0100 +++ b/src/Pure/Syntax/parser.ML Wed Feb 08 14:39:00 2006 +0100 @@ -845,7 +845,7 @@ SOME (a, prec) | _ => NONE) (Array.sub (stateset, i-1)); val allowed = - distinct (get_starts nts [] @ + gen_distinct (op =) (get_starts nts [] @ (List.mapPartial (fn (_, _, _, Terminal a :: _, _, _) => SOME a | _ => NONE) (Array.sub (stateset, i-1)))); diff -r 4efb82669880 -r f24c416a4814 src/Pure/Syntax/printer.ML --- a/src/Pure/Syntax/printer.ML Wed Feb 08 09:27:20 2006 +0100 +++ b/src/Pure/Syntax/printer.ML Wed Feb 08 14:39:00 2006 +0100 @@ -253,7 +253,7 @@ fun merge_prtabs prtabs1 prtabs2 = let - val modes = distinct (map fst (prtabs1 @ prtabs2)); + val modes = gen_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 4efb82669880 -r f24c416a4814 src/Pure/Syntax/syn_ext.ML --- a/src/Pure/Syntax/syn_ext.ML Wed Feb 08 09:27:20 2006 +0100 +++ b/src/Pure/Syntax/syn_ext.ML Wed Feb 08 14:39:00 2006 +0100 @@ -166,7 +166,7 @@ fun dels_of (XProd (_, xsymbs, _, _)) = List.mapPartial del_of xsymbs; in - map Symbol.explode (distinct (List.concat (map dels_of xprods))) + map Symbol.explode (gen_distinct (op =) (List.concat (map dels_of xprods))) end; @@ -362,12 +362,12 @@ val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes |> split_list |> apsnd (rev o List.concat); - val mfix_consts = distinct (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods); + val mfix_consts = gen_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 = distinct (map (fn (m, _, _) => m) tokentrfuns), + prmodes = gen_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 4efb82669880 -r f24c416a4814 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Wed Feb 08 09:27:20 2006 +0100 +++ b/src/Pure/Syntax/syntax.ML Wed Feb 08 14:39:00 2006 +0100 @@ -133,7 +133,7 @@ quote mode ^ " for " ^ commas_quote (map name dups))) end; in - map merge (distinct (map fst (tabs1 @ tabs2))) + map merge (gen_distinct (op =) (map fst (tabs1 @ tabs2))) end; fun extend_tokentrtab tokentrs tabs = diff -r 4efb82669880 -r f24c416a4814 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Wed Feb 08 09:27:20 2006 +0100 +++ b/src/Pure/codegen.ML Wed Feb 08 14:39:00 2006 +0100 @@ -856,7 +856,7 @@ in if module = "" then let - val modules = distinct (map (#2 o snd) code); + val modules = gen_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 4efb82669880 -r f24c416a4814 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Wed Feb 08 09:27:20 2006 +0100 +++ b/src/Pure/tactic.ML Wed Feb 08 14:39:00 2006 +0100 @@ -567,7 +567,7 @@ Returns longest lhs first to avoid folding its subexpressions.*) fun sort_lhs_depths defs = let val keylist = AList.make (term_depth o lhs_of_thm) defs - val keys = distinct (sort (rev_order o int_ord) (map #2 keylist)) + val keys = gen_distinct (op =) (sort (rev_order o int_ord) (map #2 keylist)) in map (AList.find (op =) keylist) keys end; val rev_defs = sort_lhs_depths o map symmetric;