added list update;
authorwenzelm
Sun, 29 Jul 2007 14:30:05 +0200
changeset 24049 e4adf8175149
parent 24048 a12b4faff474
child 24050 248da5f0e735
added list update;
src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Jul 29 14:30:04 2007 +0200
+++ b/src/Pure/library.ML	Sun Jul 29 14:30:05 2007 +0200
@@ -156,6 +156,7 @@
   val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
   val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
   val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
+  val update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
   val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list
   val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
   val mem: ''a * ''a list -> bool
@@ -750,6 +751,7 @@
 
 fun insert eq x xs = if member eq xs x then xs else x :: xs;
 fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs;
+fun update eq x xs = cons x (remove eq x xs);
 
 fun subtract eq = fold (remove eq);