# HG changeset patch
# User wenzelm
# Date 1194786010 -3600
# Node ID 783e5de2a6c73878a43eaedaa6a3f235089a2b1b
# Parent  8bfa6566ac6b5ff4eda2d9a2c00dca0fda6b8829
renamed update_list to cons_list;
added proper update_list (based on Library.update);

diff -r 8bfa6566ac6b -r 783e5de2a6c7 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sun Nov 11 14:00:09 2007 +0100
+++ b/src/Pure/General/table.ML	Sun Nov 11 14:00:10 2007 +0100
@@ -49,9 +49,10 @@
   val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table    (*exception DUP*)
   val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table
   val lookup_list: 'a list table -> key -> 'a list
-  val update_list: (key * 'a) -> 'a list table -> 'a list table
+  val cons_list: (key * 'a) -> 'a list table -> 'a list table
   val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
   val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table
+  val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
   val make_list: (key * 'a) list -> 'a list table
   val dest_list: 'a list table -> (key * 'a) list
   val merge_list: ('a * 'a -> bool) ->
@@ -362,16 +363,21 @@
 (* list tables *)
 
 fun lookup_list tab key = these (lookup tab key);
-fun update_list (key, x) tab = modify key (fn NONE => [x] | SOME xs => x :: xs) tab;
+
+fun cons_list (key, x) tab = modify key (fn NONE => [x] | SOME xs => x :: xs) tab;
 
 fun insert_list eq (key, x) =
   modify key (fn NONE => [x] | SOME xs => if Library.member eq xs x then raise SAME else x :: xs);
-  
+
 fun remove_list eq (key, x) tab =
   map_entry key (fn xs => (case Library.remove eq x xs of [] => raise UNDEF key | ys => ys)) tab
   handle UNDEF _ => delete key tab;
 
-fun make_list args = fold_rev update_list args empty;
+fun update_list eq (key, x) =
+  modify key (fn NONE => [x] | SOME [] => [x] | SOME (xs as y :: _) =>
+    if eq (x, y) then raise SAME else Library.update eq x xs);
+
+fun make_list args = fold_rev cons_list args empty;
 fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab);
 fun merge_list eq = join (fn _ => Library.merge eq);