--- a/src/Pure/library.ML Wed Sep 21 10:32:06 2005 +0200
+++ b/src/Pure/library.ML Wed Sep 21 10:32:24 2005 +0200
@@ -221,11 +221,7 @@
val duplicates: ''a list -> ''a list
val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
- (*association lists -- see also Pure/General/alist.ML*)
- val assoc: (''a * 'b) list * ''a -> 'b option
- val overwrite: (''a * 'b) list * (''a * 'b) -> (''a * 'b) list
-
- (*lists as tables*)
+ (*lists as tables -- see also Pure/General/alist.ML*)
val gen_merge_lists: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
val gen_merge_lists': ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
val merge_lists: ''a list -> ''a list -> ''a list
@@ -1024,19 +1020,6 @@
(** association lists **)
-(*association list lookup*)
-fun assoc ([], key) = NONE
- | assoc ((keyi, xi) :: pairs, key) =
- if key = keyi then SOME xi else assoc (pairs, key);
-
-(*association list update*)
-fun overwrite (al, p as (key, _)) =
- let fun over ((q as (keyi, _)) :: pairs) =
- if keyi = key then p :: pairs else q :: (over pairs)
- | over [] = [p]
- in over al end;
-
-
(* lists as tables *)
fun gen_merge_lists _ xs [] = xs