introduced gen_distinct in place of distinct
authorhaftmann
Wed Feb 08 14:39:00 2006 +0100 (2006-02-08)
changeset 18977f24c416a4814
parent 18976 4efb82669880
child 18978 8971c306b94f
introduced gen_distinct in place of distinct
src/FOLP/IFOLP.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/induct_attrib.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syntax.ML
src/Pure/codegen.ML
src/Pure/tactic.ML
     1.1 --- a/src/FOLP/IFOLP.ML	Wed Feb 08 09:27:20 2006 +0100
     1.2 +++ b/src/FOLP/IFOLP.ML	Wed Feb 08 14:39:00 2006 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4            and concl = discard_proof (Logic.strip_assums_concl prem)
     1.5        in
     1.6            if exists (fn hyp => hyp aconv concl) hyps
     1.7 -          then case distinct (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of
     1.8 +          then case gen_distinct (op =) (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of
     1.9                     [_] => assume_tac i
    1.10                   |  _  => no_tac
    1.11            else no_tac
     2.1 --- a/src/Pure/Isar/attrib.ML	Wed Feb 08 09:27:20 2006 +0100
     2.2 +++ b/src/Pure/Isar/attrib.ML	Wed Feb 08 14:39:00 2006 +0100
     2.3 @@ -253,7 +253,7 @@
     2.4      fun prepT (a, T) = (Thm.ctyp_of thy (TVar (a, the_sort sorts a)), Thm.ctyp_of thy T);
     2.5      fun prep (xi, t) = pairself (Thm.cterm_of thy) (Var (xi, Term.fastype_of t), t);
     2.6    in
     2.7 -    Drule.instantiate (map prepT (distinct envT),
     2.8 +    Drule.instantiate (map prepT (gen_distinct (op =) envT),
     2.9        map prep (gen_distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) thm
    2.10    end;
    2.11  
     3.1 --- a/src/Pure/Isar/context_rules.ML	Wed Feb 08 09:27:20 2006 +0100
     3.2 +++ b/src/Pure/Isar/context_rules.ML	Wed Feb 08 14:39:00 2006 +0100
     3.3 @@ -59,7 +59,7 @@
     3.4    (elim_queryK, "extra elimination rules (elim?)")];
     3.5  
     3.6  val rule_kinds = map #1 kind_names;
     3.7 -val rule_indexes = distinct (map #1 rule_kinds);
     3.8 +val rule_indexes = gen_distinct (op =) (map #1 rule_kinds);
     3.9  
    3.10  
    3.11  (* context data *)
     4.1 --- a/src/Pure/Isar/induct_attrib.ML	Wed Feb 08 09:27:20 2006 +0100
     4.2 +++ b/src/Pure/Isar/induct_attrib.ML	Wed Feb 08 14:39:00 2006 +0100
     4.3 @@ -55,7 +55,7 @@
     4.4  
     4.5  fun vars_of tm =
     4.6    Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []
     4.7 -  |> Library.distinct
     4.8 +  |> gen_distinct (op =)
     4.9    |> rev;
    4.10  
    4.11  local
     5.1 --- a/src/Pure/Syntax/parser.ML	Wed Feb 08 09:27:20 2006 +0100
     5.2 +++ b/src/Pure/Syntax/parser.ML	Wed Feb 08 14:39:00 2006 +0100
     5.3 @@ -845,7 +845,7 @@
     5.4                             SOME (a, prec) | _ => NONE)
     5.5                            (Array.sub (stateset, i-1));
     5.6                val allowed =
     5.7 -                distinct (get_starts nts [] @
     5.8 +                gen_distinct (op =) (get_starts nts [] @
     5.9                    (List.mapPartial (fn (_, _, _, Terminal a :: _, _, _) => SOME a
    5.10                                 | _ => NONE)
    5.11                               (Array.sub (stateset, i-1))));
     6.1 --- a/src/Pure/Syntax/printer.ML	Wed Feb 08 09:27:20 2006 +0100
     6.2 +++ b/src/Pure/Syntax/printer.ML	Wed Feb 08 14:39:00 2006 +0100
     6.3 @@ -253,7 +253,7 @@
     6.4  
     6.5  fun merge_prtabs prtabs1 prtabs2 =
     6.6    let
     6.7 -    val modes = distinct (map fst (prtabs1 @ prtabs2));
     6.8 +    val modes = gen_distinct (op =) (map fst (prtabs1 @ prtabs2));
     6.9      fun merge m = (m, Symtab.merge_list (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m));
    6.10    in map merge modes end;
    6.11  
     7.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Feb 08 09:27:20 2006 +0100
     7.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Feb 08 14:39:00 2006 +0100
     7.3 @@ -166,7 +166,7 @@
     7.4      fun dels_of (XProd (_, xsymbs, _, _)) =
     7.5        List.mapPartial del_of xsymbs;
     7.6    in
     7.7 -    map Symbol.explode (distinct (List.concat (map dels_of xprods)))
     7.8 +    map Symbol.explode (gen_distinct (op =) (List.concat (map dels_of xprods)))
     7.9    end;
    7.10  
    7.11  
    7.12 @@ -362,12 +362,12 @@
    7.13  
    7.14      val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
    7.15        |> split_list |> apsnd (rev o List.concat);
    7.16 -    val mfix_consts = distinct (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
    7.17 +    val mfix_consts = gen_distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
    7.18    in
    7.19      SynExt {
    7.20        xprods = xprods,
    7.21        consts = consts union_string mfix_consts,
    7.22 -      prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
    7.23 +      prmodes = gen_distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
    7.24        parse_ast_translation = parse_ast_translation,
    7.25        parse_rules = parse_rules' @ parse_rules,
    7.26        parse_translation = parse_translation,
     8.1 --- a/src/Pure/Syntax/syntax.ML	Wed Feb 08 09:27:20 2006 +0100
     8.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Feb 08 14:39:00 2006 +0100
     8.3 @@ -133,7 +133,7 @@
     8.4              quote mode ^ " for " ^ commas_quote (map name dups)))
     8.5        end;
     8.6    in
     8.7 -    map merge (distinct (map fst (tabs1 @ tabs2)))
     8.8 +    map merge (gen_distinct (op =) (map fst (tabs1 @ tabs2)))
     8.9    end;
    8.10  
    8.11  fun extend_tokentrtab tokentrs tabs =
     9.1 --- a/src/Pure/codegen.ML	Wed Feb 08 09:27:20 2006 +0100
     9.2 +++ b/src/Pure/codegen.ML	Wed Feb 08 14:39:00 2006 +0100
     9.3 @@ -856,7 +856,7 @@
     9.4    in
     9.5      if module = "" then
     9.6        let
     9.7 -        val modules = distinct (map (#2 o snd) code);
     9.8 +        val modules = gen_distinct (op =) (map (#2 o snd) code);
     9.9          val mod_gr = foldr (uncurry Graph.add_edge_acyclic)
    9.10            (foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules)
    9.11            (List.concat (map (fn (s, (_, module, _)) => map (pair module)
    10.1 --- a/src/Pure/tactic.ML	Wed Feb 08 09:27:20 2006 +0100
    10.2 +++ b/src/Pure/tactic.ML	Wed Feb 08 14:39:00 2006 +0100
    10.3 @@ -567,7 +567,7 @@
    10.4    Returns longest lhs first to avoid folding its subexpressions.*)
    10.5  fun sort_lhs_depths defs =
    10.6    let val keylist = AList.make (term_depth o lhs_of_thm) defs
    10.7 -      val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
    10.8 +      val keys = gen_distinct (op =) (sort (rev_order o int_ord) (map #2 keylist))
    10.9    in map (AList.find (op =) keylist) keys end;
   10.10  
   10.11  val rev_defs = sort_lhs_depths o map symmetric;