src/Pure/library.ML
changeset 17540 f662416aa5f2
parent 17498 d83af87bbdc5
child 17545 1ba448f96af1
     1.1 --- a/src/Pure/library.ML	Wed Sep 21 10:32:06 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Sep 21 10:32:24 2005 +0200
     1.3 @@ -221,11 +221,7 @@
     1.4    val duplicates: ''a list -> ''a list
     1.5    val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
     1.6  
     1.7 -  (*association lists -- see also Pure/General/alist.ML*)
     1.8 -  val assoc: (''a * 'b) list * ''a -> 'b option
     1.9 -  val overwrite: (''a * 'b) list * (''a * 'b) -> (''a * 'b) list
    1.10 -
    1.11 -  (*lists as tables*)
    1.12 +  (*lists as tables -- see also Pure/General/alist.ML*)
    1.13    val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
    1.14    val gen_merge_lists': ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
    1.15    val merge_lists: ''a list -> ''a list -> ''a list
    1.16 @@ -1024,19 +1020,6 @@
    1.17  
    1.18  (** association lists **)
    1.19  
    1.20 -(*association list lookup*)
    1.21 -fun assoc ([], key) = NONE
    1.22 -  | assoc ((keyi, xi) :: pairs, key) =
    1.23 -      if key = keyi then SOME xi else assoc (pairs, key);
    1.24 -
    1.25 -(*association list update*)
    1.26 -fun overwrite (al, p as (key, _)) =
    1.27 -  let fun over ((q as (keyi, _)) :: pairs) =
    1.28 -            if keyi = key then p :: pairs else q :: (over pairs)
    1.29 -        | over [] = [p]
    1.30 -  in over al end;
    1.31 -
    1.32 -
    1.33  (* lists as tables *)
    1.34  
    1.35  fun gen_merge_lists _ xs [] = xs