introduced gen_distinct in place of distinct

--- 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

--- 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;
 

--- 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 *)

--- 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

--- 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))));

--- 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;
 

--- 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,

--- 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 =

--- 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)

--- 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;