removed distinct, renamed gen_distinct to distinct;
authorwenzelm
Wed Feb 15 21:34:55 2006 +0100 (2006-02-15 ago)
changeset 19046bc5c6c9b114e
parent 19045 75786c2eb897
child 19047 670ce193b618
removed distinct, renamed gen_distinct to distinct;
TFL/tfl.ML
TFL/usyntax.ML
src/FOLP/IFOLP.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/inductive_codegen.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/record_package.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/find_theorems.ML
src/Pure/Isar/induct_attrib.ML
src/Pure/Isar/method.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/present.ML
src/Pure/codegen.ML
src/Pure/context.ML
src/Pure/library.ML
src/Pure/pure_thy.ML
src/Pure/type_infer.ML
     1.1 --- a/TFL/tfl.ML	Wed Feb 15 19:11:10 2006 +0100
     1.2 +++ b/TFL/tfl.ML	Wed Feb 15 21:34:55 2006 +0100
     1.3 @@ -316,7 +316,7 @@
     1.4          | single [f] = f
     1.5          | single fs  =
     1.6                (*multiple function names?*)
     1.7 -              if length (gen_distinct same_name fs) < length fs
     1.8 +              if length (distinct same_name fs) < length fs
     1.9                then mk_functional_err
    1.10                     "The function being declared appears with multiple types"
    1.11                else mk_functional_err
    1.12 @@ -328,7 +328,7 @@
    1.13                     handle TERM _ => raise TFL_ERR "mk_functional"
    1.14                          "recursion equations must use the = relation")
    1.15       val (funcs,pats) = ListPair.unzip (map (fn (t$u) =>(t,u)) L)
    1.16 -     val atom = single (gen_distinct (op aconv) funcs)
    1.17 +     val atom = single (distinct (op aconv) funcs)
    1.18       val (fname,ftype) = dest_atom atom
    1.19       val dummy = map (no_repeat_vars thy) pats
    1.20       val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
     2.1 --- a/TFL/usyntax.ML	Wed Feb 15 19:11:10 2006 +0100
     2.2 +++ b/TFL/usyntax.ML	Wed Feb 15 21:34:55 2006 +0100
     2.3 @@ -115,7 +115,7 @@
     2.4  val is_vartype = can dest_vtype;
     2.5  
     2.6  val type_vars  = map mk_prim_vartype o typ_tvars
     2.7 -fun type_varsl L = distinct (fold (curry op @ o type_vars) L []);
     2.8 +fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []);
     2.9  
    2.10  val alpha  = mk_vartype "'a"
    2.11  val beta   = mk_vartype "'b"
     3.1 --- a/src/FOLP/IFOLP.ML	Wed Feb 15 19:11:10 2006 +0100
     3.2 +++ b/src/FOLP/IFOLP.ML	Wed Feb 15 21:34:55 2006 +0100
     3.3 @@ -77,7 +77,7 @@
     3.4            and concl = discard_proof (Logic.strip_assums_concl prem)
     3.5        in
     3.6            if exists (fn hyp => hyp aconv concl) hyps
     3.7 -          then case gen_distinct (op =) (List.filter (fn hyp=> could_unify(hyp,concl)) hyps) of
     3.8 +          then case distinct (op =) (filter (fn hyp => could_unify (hyp, concl)) hyps) of
     3.9                     [_] => assume_tac i
    3.10                   |  _  => no_tac
    3.11            else no_tac
     4.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Feb 15 19:11:10 2006 +0100
     4.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Feb 15 21:34:55 2006 +0100
     4.3 @@ -158,9 +158,8 @@
     4.4  
     4.5  (* get names of clasimp axioms used*)
     4.6  fun get_axiom_names step_nums clause_arr =
     4.7 -  distinct (sort_strings 
     4.8 -            (map (ResClause.get_axiomName o #1) 
     4.9 -	     (get_clasimp_cls clause_arr step_nums)));   
    4.10 +  sort_distinct string_ord
    4.11 +    (map (ResClause.get_axiomName o #1) (get_clasimp_cls clause_arr step_nums));
    4.12  
    4.13   (*String contains multiple lines. We want those of the form 
    4.14       "253[0:Inp] et cetera..."
    4.15 @@ -221,13 +220,13 @@
    4.16       
    4.17       val vars = map thm_vars clauses
    4.18      
    4.19 -     val distvars = distinct (fold append vars [])
    4.20 +     val distvars = distinct (op =) (fold append vars [])
    4.21       val clause_terms = map prop_of clauses  
    4.22       val clause_frees = List.concat (map term_frees clause_terms)
    4.23  
    4.24       val frees = map lit_string_with_nums clause_frees;
    4.25  
    4.26 -     val distfrees = distinct frees
    4.27 +     val distfrees = distinct (op =) frees
    4.28  
    4.29       val metas = map Meson.make_meta_clause clauses
    4.30       val ax_strs = map #3 axioms
     5.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Feb 15 19:11:10 2006 +0100
     5.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Feb 15 21:34:55 2006 +0100
     5.3 @@ -326,7 +326,7 @@
     5.4  fun dt_cases (descr: descr) (_, args, constrs) =
     5.5    let
     5.6      fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
     5.7 -    val bnames = map the_bname (distinct (List.concat (map dt_recs args)));
     5.8 +    val bnames = map the_bname (distinct (op =) (List.concat (map dt_recs args)));
     5.9    in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
    5.10  
    5.11  
    5.12 @@ -492,7 +492,7 @@
    5.13              ([], true, SOME _) =>
    5.14                case_error "Extra '_' dummy pattern" (SOME tname) [u]
    5.15            | (_ :: _, _, _) =>
    5.16 -              let val extra = distinct (map (fst o fst) cases'')
    5.17 +              let val extra = distinct (op =) (map (fst o fst) cases'')
    5.18                in case extra \\ map fst constrs of
    5.19                    [] => case_error ("More than one clause for constructor(s) " ^
    5.20                      commas extra) (SOME tname) [u]
     6.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Feb 15 19:11:10 2006 +0100
     6.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Feb 15 21:34:55 2006 +0100
     6.3 @@ -177,7 +177,7 @@
     6.4      string_of_mode ms)) modes));
     6.5  
     6.6  val term_vs = map (fst o fst o dest_Var) o term_vars;
     6.7 -val terms_vs = distinct o List.concat o (map term_vs);
     6.8 +val terms_vs = distinct (op =) o List.concat o (map term_vs);
     6.9  
    6.10  (** collect all Vars in a term (with duplicates!) **)
    6.11  fun term_vTs tm =
    6.12 @@ -441,7 +441,7 @@
    6.13            end
    6.14        | compile_prems out_ts vs names gr ps =
    6.15            let
    6.16 -            val vs' = distinct (List.concat (vs :: map term_vs out_ts));
    6.17 +            val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts));
    6.18              val SOME (p, mode as SOME (Mode ((_, js), _))) =
    6.19                select_mode_prem thy modes' vs' ps;
    6.20              val ps' = filter_out (equal p) ps;
     7.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Feb 15 19:11:10 2006 +0100
     7.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Feb 15 21:34:55 2006 +0100
     7.3 @@ -324,7 +324,7 @@
     7.4        ||> Extraction.add_typeof_eqns_i ty_eqs
     7.5        ||> Extraction.add_realizes_eqns_i rlz_eqs;
     7.6      fun get f = (these oo Option.map) f;
     7.7 -    val rec_names = distinct (map (fst o dest_Const o head_of o fst o
     7.8 +    val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
     7.9        HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
    7.10      val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) =>
    7.11        if s mem rsets then
    7.12 @@ -341,7 +341,7 @@
    7.13          c (prop_of (forall_intr_list (map (cterm_of (sign_of thy2) o Var)
    7.14            (rev (Term.add_vars (prop_of intr) []) \\ params')) intr))))
    7.15              (intrs ~~ List.concat constrss);
    7.16 -    val rlzsets = distinct (map (fn rintr => snd (HOLogic.dest_mem
    7.17 +    val rlzsets = distinct (op =) (map (fn rintr => snd (HOLogic.dest_mem
    7.18        (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)))) rintrs);
    7.19  
    7.20      (** realizability predicate **)
     8.1 --- a/src/HOL/Tools/meson.ML	Wed Feb 15 19:11:10 2006 +0100
     8.2 +++ b/src/HOL/Tools/meson.ML	Wed Feb 15 21:34:55 2006 +0100
     8.3 @@ -420,7 +420,7 @@
     8.4  (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
     8.5  fun make_horns ths =
     8.6      name_thms "Horn#"
     8.7 -      (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
     8.8 +      (distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
     8.9  
    8.10  (*Could simply use nprems_of, which would count remaining subgoals -- no
    8.11    discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)
    8.12 @@ -525,7 +525,7 @@
    8.13  
    8.14  fun make_meta_clauses ths =
    8.15      name_thms "MClause#"
    8.16 -      (gen_distinct Drule.eq_thm_prop (map make_meta_clause ths));
    8.17 +      (distinct Drule.eq_thm_prop (map make_meta_clause ths));
    8.18  
    8.19  (*Permute a rule's premises to move the i-th premise to the last position.*)
    8.20  fun make_last i th =
     9.1 --- a/src/HOL/Tools/primrec_package.ML	Wed Feb 15 19:11:10 2006 +0100
     9.2 +++ b/src/HOL/Tools/primrec_package.ML	Wed Feb 15 21:34:55 2006 +0100
     9.3 @@ -227,7 +227,7 @@
     9.4      val sg = Theory.sign_of thy;
     9.5      val dt_info = DatatypePackage.get_datatypes thy;
     9.6      val rec_eqns = foldr (process_eqn sg) [] (map snd eqns);
     9.7 -    val tnames = distinct (map (#1 o snd) rec_eqns);
     9.8 +    val tnames = distinct (op =) (map (#1 o snd) rec_eqns);
     9.9      val dts = find_dts dt_info tnames tnames;
    9.10      val main_fns = 
    9.11        map (fn (tname, {index, ...}) =>
    10.1 --- a/src/HOL/Tools/record_package.ML	Wed Feb 15 19:11:10 2006 +0100
    10.2 +++ b/src/HOL/Tools/record_package.ML	Wed Feb 15 21:34:55 2006 +0100
    10.3 @@ -1665,7 +1665,8 @@
    10.4  
    10.5      (* prepare print translation functions *)
    10.6      val field_tr's =
    10.7 -      print_translation (distinct (List.concat (map NameSpace.accesses' (full_moreN :: names))));
    10.8 +      print_translation (distinct (op =)
    10.9 +        (List.concat (map NameSpace.accesses' (full_moreN :: names))));
   10.10  
   10.11      val adv_ext_tr's =
   10.12      let
    11.1 --- a/src/Pure/Isar/attrib.ML	Wed Feb 15 19:11:10 2006 +0100
    11.2 +++ b/src/Pure/Isar/attrib.ML	Wed Feb 15 21:34:55 2006 +0100
    11.3 @@ -238,8 +238,8 @@
    11.4      fun prepT (a, T) = (Thm.ctyp_of thy (TVar (a, the_sort sorts a)), Thm.ctyp_of thy T);
    11.5      fun prep (xi, t) = pairself (Thm.cterm_of thy) (Var (xi, Term.fastype_of t), t);
    11.6    in
    11.7 -    Drule.instantiate (map prepT (gen_distinct (op =) envT),
    11.8 -      map prep (gen_distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) thm
    11.9 +    Drule.instantiate (map prepT (distinct (op =) envT),
   11.10 +      map prep (distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) thm
   11.11    end;
   11.12  
   11.13  in
    12.1 --- a/src/Pure/Isar/context_rules.ML	Wed Feb 15 19:11:10 2006 +0100
    12.2 +++ b/src/Pure/Isar/context_rules.ML	Wed Feb 15 21:34:55 2006 +0100
    12.3 @@ -59,7 +59,7 @@
    12.4    (elim_queryK, "extra elimination rules (elim?)")];
    12.5  
    12.6  val rule_kinds = map #1 kind_names;
    12.7 -val rule_indexes = gen_distinct (op =) (map #1 rule_kinds);
    12.8 +val rule_indexes = distinct (op =) (map #1 rule_kinds);
    12.9  
   12.10  
   12.11  (* context data *)
    13.1 --- a/src/Pure/Isar/find_theorems.ML	Wed Feb 15 19:11:10 2006 +0100
    13.2 +++ b/src/Pure/Isar/find_theorems.ML	Wed Feb 15 21:34:55 2006 +0100
    13.3 @@ -242,7 +242,7 @@
    13.4    (ProofContext.lthms_containing ctxt spec
    13.5      |> map PureThy.selections
    13.6      |> List.concat
    13.7 -    |> gen_distinct (fn ((r1, th1), (r2, th2)) =>
    13.8 +    |> distinct (fn ((r1, th1), (r2, th2)) =>
    13.9          r1 = r2 andalso Drule.eq_thm_prop (th1, th2)));
   13.10  
   13.11  fun print_theorems ctxt opt_goal opt_limit raw_criteria =
    14.1 --- a/src/Pure/Isar/induct_attrib.ML	Wed Feb 15 19:11:10 2006 +0100
    14.2 +++ b/src/Pure/Isar/induct_attrib.ML	Wed Feb 15 21:34:55 2006 +0100
    14.3 @@ -54,9 +54,7 @@
    14.4  (* variables -- ordered left-to-right, preferring right *)
    14.5  
    14.6  fun vars_of tm =
    14.7 -  Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []
    14.8 -  |> gen_distinct (op =)
    14.9 -  |> rev;
   14.10 +  rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm []));
   14.11  
   14.12  local
   14.13  
    15.1 --- a/src/Pure/Isar/method.ML	Wed Feb 15 19:11:10 2006 +0100
    15.2 +++ b/src/Pure/Isar/method.ML	Wed Feb 15 21:34:55 2006 +0100
    15.3 @@ -290,7 +290,7 @@
    15.4  
    15.5  val remdups_tac = SUBGOAL (fn (g, i) =>
    15.6    let val prems = Logic.strip_assums_hyp g in
    15.7 -    REPEAT_DETERM_N (length prems - length (gen_distinct op aconv prems))
    15.8 +    REPEAT_DETERM_N (length prems - length (distinct op aconv prems))
    15.9      (Tactic.ematch_tac [Drule.remdups_rl] i THEN Tactic.eq_assume_tac i)
   15.10    end);
   15.11  
   15.12 @@ -393,7 +393,7 @@
   15.13            map
   15.14              (fn (xi, t) =>
   15.15                pairself (Thm.cterm_of thy) (Var (xi, fastype_of t), t))
   15.16 -            (gen_distinct
   15.17 +            (distinct
   15.18                (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2)
   15.19                (xis ~~ ts));
   15.20          (* Lift and instantiate rule *)
    16.1 --- a/src/Pure/Isar/rule_cases.ML	Wed Feb 15 19:11:10 2006 +0100
    16.2 +++ b/src/Pure/Isar/rule_cases.ML	Wed Feb 15 21:34:55 2006 +0100
    16.3 @@ -130,7 +130,7 @@
    16.4    in
    16.5      if len = 0 then NONE
    16.6      else if len = 1 then SOME (common_case (hd cases))
    16.7 -    else if is_none case_outline orelse length (gen_distinct (op =) (map fst cases)) > 1 then NONE
    16.8 +    else if is_none case_outline orelse length (distinct (op =) (map fst cases)) > 1 then NONE
    16.9      else SOME (nested_case (hd cases))
   16.10    end;
   16.11  
    17.1 --- a/src/Pure/Syntax/parser.ML	Wed Feb 15 19:11:10 2006 +0100
    17.2 +++ b/src/Pure/Syntax/parser.ML	Wed Feb 15 21:34:55 2006 +0100
    17.3 @@ -845,7 +845,7 @@
    17.4                             SOME (a, prec) | _ => NONE)
    17.5                            (Array.sub (stateset, i-1));
    17.6                val allowed =
    17.7 -                gen_distinct (op =) (get_starts nts [] @
    17.8 +                distinct (op =) (get_starts nts [] @
    17.9                    (List.mapPartial (fn (_, _, _, Terminal a :: _, _, _) => SOME a
   17.10                                 | _ => NONE)
   17.11                               (Array.sub (stateset, i-1))));
    18.1 --- a/src/Pure/Syntax/printer.ML	Wed Feb 15 19:11:10 2006 +0100
    18.2 +++ b/src/Pure/Syntax/printer.ML	Wed Feb 15 21:34:55 2006 +0100
    18.3 @@ -253,7 +253,7 @@
    18.4  
    18.5  fun merge_prtabs prtabs1 prtabs2 =
    18.6    let
    18.7 -    val modes = gen_distinct (op =) (map fst (prtabs1 @ prtabs2));
    18.8 +    val modes = distinct (op =) (map fst (prtabs1 @ prtabs2));
    18.9      fun merge m = (m, Symtab.merge_list (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m));
   18.10    in map merge modes end;
   18.11  
    19.1 --- a/src/Pure/Syntax/syn_ext.ML	Wed Feb 15 19:11:10 2006 +0100
    19.2 +++ b/src/Pure/Syntax/syn_ext.ML	Wed Feb 15 21:34:55 2006 +0100
    19.3 @@ -361,12 +361,13 @@
    19.4  
    19.5      val (xprods, parse_rules') = map (mfix_to_xprod convert is_logtype) mfixes
    19.6        |> split_list |> apsnd (rev o List.concat);
    19.7 -    val mfix_consts = gen_distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
    19.8 +    val mfix_consts =
    19.9 +      distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
   19.10    in
   19.11      SynExt {
   19.12        xprods = xprods,
   19.13        consts = consts union_string mfix_consts,
   19.14 -      prmodes = gen_distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
   19.15 +      prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
   19.16        parse_ast_translation = parse_ast_translation,
   19.17        parse_rules = parse_rules' @ parse_rules,
   19.18        parse_translation = parse_translation,
    20.1 --- a/src/Pure/Syntax/syntax.ML	Wed Feb 15 19:11:10 2006 +0100
    20.2 +++ b/src/Pure/Syntax/syntax.ML	Wed Feb 15 21:34:55 2006 +0100
    20.3 @@ -111,7 +111,7 @@
    20.4  (** tables of token translation functions **)
    20.5  
    20.6  fun lookup_tokentr tabs modes =
    20.7 -  let val trs = gen_distinct (eq_fst (op =))
    20.8 +  let val trs = distinct (eq_fst (op =))
    20.9      (List.concat (map (these o AList.lookup (op =) tabs) (modes @ [""])))
   20.10    in fn c => Option.map fst (AList.lookup (op =) trs c) end;
   20.11  
   20.12 @@ -125,16 +125,14 @@
   20.13        let
   20.14          val trs1 = these (AList.lookup (op =) tabs1 mode);
   20.15          val trs2 = these (AList.lookup (op =) tabs2 mode);
   20.16 -        val trs = gen_distinct eq_tr (trs1 @ trs2);
   20.17 +        val trs = distinct eq_tr (trs1 @ trs2);
   20.18        in
   20.19          (case duplicates (eq_fst (op =)) trs of
   20.20            [] => (mode, trs)
   20.21          | dups => error ("More than one token translation function in mode " ^
   20.22              quote mode ^ " for " ^ commas_quote (map name dups)))
   20.23        end;
   20.24 -  in
   20.25 -    map merge (gen_distinct (op =) (map fst (tabs1 @ tabs2)))
   20.26 -  end;
   20.27 +  in map merge (distinct (op =) (map fst (tabs1 @ tabs2))) end;
   20.28  
   20.29  fun extend_tokentrtab tokentrs tabs =
   20.30    let
    21.1 --- a/src/Pure/Thy/present.ML	Wed Feb 15 19:11:10 2006 +0100
    21.2 +++ b/src/Pure/Thy/present.ML	Wed Feb 15 21:34:55 2006 +0100
    21.3 @@ -273,7 +273,7 @@
    21.4    | _ => error ("Malformed document version specification: " ^ quote str));
    21.5  
    21.6  fun read_versions strs =
    21.7 -  rev (gen_distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
    21.8 +  rev (distinct (eq_fst (op =)) (rev ((documentN, "") :: map read_version strs)))
    21.9    |> filter_out (equal "-" o #2);
   21.10  
   21.11  
    22.1 --- a/src/Pure/codegen.ML	Wed Feb 15 19:11:10 2006 +0100
    22.2 +++ b/src/Pure/codegen.ML	Wed Feb 15 21:34:55 2006 +0100
    22.3 @@ -856,7 +856,7 @@
    22.4    in
    22.5      if module = "" then
    22.6        let
    22.7 -        val modules = gen_distinct (op =) (map (#2 o snd) code);
    22.8 +        val modules = distinct (op =) (map (#2 o snd) code);
    22.9          val mod_gr = foldr (uncurry Graph.add_edge_acyclic)
   22.10            (foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules)
   22.11            (List.concat (map (fn (s, (_, module, _)) => map (pair module)
    23.1 --- a/src/Pure/context.ML	Wed Feb 15 19:11:10 2006 +0100
    23.2 +++ b/src/Pure/context.ML	Wed Feb 15 21:34:55 2006 +0100
    23.3 @@ -379,8 +379,8 @@
    23.4    else
    23.5      let
    23.6        val parents =
    23.7 -        maximal_thys (gen_distinct eq_thy (map check_thy imports));
    23.8 -      val ancestors = gen_distinct eq_thy (parents @ List.concat (map ancestors_of parents));
    23.9 +        maximal_thys (distinct eq_thy (map check_thy imports));
   23.10 +      val ancestors = distinct eq_thy (parents @ List.concat (map ancestors_of parents));
   23.11        val Theory ({id, ids, iids, ...}, data, _, _) =
   23.12          (case parents of
   23.13            [] => error "No parent theories"
    24.1 --- a/src/Pure/library.ML	Wed Feb 15 19:11:10 2006 +0100
    24.2 +++ b/src/Pure/library.ML	Wed Feb 15 21:34:55 2006 +0100
    24.3 @@ -214,9 +214,8 @@
    24.4    val \\ : ''a list * ''a list -> ''a list
    24.5    val gen_rem: ('a * 'b -> bool) -> 'a list * 'b -> 'a list
    24.6    val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
    24.7 -  val gen_distinct: ('a * 'a -> bool) -> 'a list -> 'a list
    24.8 -  val distinct: ''a list -> ''a list
    24.9    val findrep: ''a list -> ''a list
   24.10 +  val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
   24.11    val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
   24.12    val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
   24.13  
   24.14 @@ -1011,24 +1010,20 @@
   24.15  fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
   24.16  fun gen_rems eq (xs, ys) = filter_out (member eq ys) xs;
   24.17  
   24.18 +(*returns the tail beginning with the first repeated element, or []*)
   24.19 +fun findrep [] = []
   24.20 +  | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
   24.21 +
   24.22 +
   24.23  (*makes a list of the distinct members of the input; preserves order, takes
   24.24    first of equal elements*)
   24.25 -fun gen_distinct eq lst =
   24.26 +fun distinct eq lst =
   24.27    let
   24.28      fun dist (rev_seen, []) = rev rev_seen
   24.29        | dist (rev_seen, x :: xs) =
   24.30            if member eq rev_seen x then dist (rev_seen, xs)
   24.31            else dist (x :: rev_seen, xs);
   24.32 -  in
   24.33 -    dist ([], lst)
   24.34 -  end;
   24.35 -
   24.36 -fun distinct l = gen_distinct (op =) l;
   24.37 -
   24.38 -(*returns the tail beginning with the first repeated element, or []*)
   24.39 -fun findrep [] = []
   24.40 -  | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
   24.41 -
   24.42 +  in dist ([], lst) end;
   24.43  
   24.44  (*returns a list containing all repeated elements exactly once; preserves
   24.45    order, takes first of equal elements*)
    25.1 --- a/src/Pure/pure_thy.ML	Wed Feb 15 19:11:10 2006 +0100
    25.2 +++ b/src/Pure/pure_thy.ML	Wed Feb 15 21:34:55 2006 +0100
    25.3 @@ -312,7 +312,7 @@
    25.4    |> map (fn thy =>
    25.5        FactIndex.find (fact_index_of thy) spec
    25.6        |> List.filter (fn (name, ths) => valid_thms theory (Name name, ths))
    25.7 -      |> gen_distinct (eq_fst (op =)))
    25.8 +      |> distinct (eq_fst (op =)))
    25.9    |> List.concat;
   25.10  
   25.11  fun thms_containing_consts thy consts =
    26.1 --- a/src/Pure/type_infer.ML	Wed Feb 15 19:11:10 2006 +0100
    26.2 +++ b/src/Pure/type_infer.ML	Wed Feb 15 21:34:55 2006 +0100
    26.3 @@ -461,7 +461,7 @@
    26.4      fun eq ((xi: indexname, S), (xi', S')) =
    26.5        xi = xi' andalso Type.eq_sort tsig (S, S');
    26.6  
    26.7 -    val env = gen_distinct eq (map (apsnd map_sort) raw_env);
    26.8 +    val env = distinct eq (map (apsnd map_sort) raw_env);
    26.9      val _ = (case duplicates (eq_fst (op =)) env of [] => ()
   26.10        | dups => error ("Inconsistent sort constraints for type variable(s) "
   26.11            ^ commas_quote (map (Syntax.string_of_vname' o fst) dups)));