removed distinct_fst_string;
authorwenzelm
Mon Dec 29 14:29:34 1997 +0100 (1997-12-29)
changeset 449616187138463d
parent 4495 8648ba842d14
child 4497 2ba0730672c9
removed distinct_fst_string;
src/Pure/Syntax/syntax.ML
src/Pure/Thy/thy_parse.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sun Dec 28 15:47:09 1997 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Dec 29 14:29:34 1997 +0100
     1.3 @@ -96,7 +96,7 @@
     1.4  (** tables of token translation functions **)
     1.5  
     1.6  fun lookup_tokentr tabs modes =
     1.7 -  let val trs = distinct_fst_string (flat (map (assocs tabs) (modes @ [""])))
     1.8 +  let val trs = gen_distinct eq_fst (flat (map (assocs tabs) (modes @ [""])))
     1.9    in fn c => apsome fst (assoc (trs, c)) end;
    1.10  
    1.11  fun merge_tokentrtabs tabs1 tabs2 =
     2.1 --- a/src/Pure/Thy/thy_parse.ML	Sun Dec 28 15:47:09 1997 +0100
     2.2 +++ b/src/Pure/Thy/thy_parse.ML	Mon Dec 29 14:29:34 1997 +0100
     2.3 @@ -436,7 +436,7 @@
     2.4  fun make_syntax keywords sects =
     2.5    let
     2.6      val dups = duplicates (map fst sects);
     2.7 -    val sects' = distinct_fst_string sects;
     2.8 +    val sects' = gen_distinct eq_fst sects;
     2.9    in
    2.10      if null dups then ()
    2.11      else warning ("Duplicate declaration of theory file sections:\n" ^ commas_quote dups);
     3.1 --- a/src/Pure/library.ML	Sun Dec 28 15:47:09 1997 +0100
     3.2 +++ b/src/Pure/library.ML	Mon Dec 29 14:29:34 1997 +0100
     3.3 @@ -553,20 +553,6 @@
     3.4  
     3.5  fun distinct l = gen_distinct (op =) l;
     3.6  
     3.7 -(*tuned version of distinct -- eq wrt. strings in fst component*)
     3.8 -fun distinct_fst_string lst =
     3.9 -  let
    3.10 -    fun mem_str ((_:string, _), []) = false
    3.11 -      | mem_str (p as (x, _), ((y, _) :: qs)) = x = y orelse mem_str (p, qs);
    3.12 -
    3.13 -    fun dist (rev_seen, []) = rev rev_seen
    3.14 -      | dist (rev_seen, p :: ps) =
    3.15 -          if mem_str (p, rev_seen) then dist (rev_seen, ps)
    3.16 -          else dist (p :: rev_seen, ps);
    3.17 -  in
    3.18 -    dist ([], lst)
    3.19 -  end;
    3.20 -
    3.21  
    3.22  (*returns the tail beginning with the first repeated element, or []*)
    3.23  fun findrep [] = []