1.1 --- a/src/Pure/library.ML	Sun Jul 29 14:30:04 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Sun Jul 29 14:30:05 2007 +0200
     1.3 @@ -156,6 +156,7 @@
     1.4    val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
     1.5    val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
     1.6    val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
     1.7 +  val update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
     1.8    val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list
     1.9    val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
    1.10    val mem: ''a * ''a list -> bool
    1.11 @@ -750,6 +751,7 @@
    1.12  
    1.13  fun insert eq x xs = if member eq xs x then xs else x :: xs;
    1.14  fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs;
    1.15 +fun update eq x xs = cons x (remove eq x xs);
    1.16  
    1.17  fun subtract eq = fold (remove eq);
    1.18