# HG changeset patch
# User wenzelm
# Date 1146345408 -7200
# Node ID 980a2edf9e8244fd14c33e022d7cba4f590c066f
# Parent  0b345cf953c4377e3b20440fb241f4d1e9560ea9
added insert_list;

diff -r 0b345cf953c4 -r 980a2edf9e82 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sat Apr 29 23:16:47 2006 +0200
+++ b/src/Pure/General/table.ML	Sat Apr 29 23:16:48 2006 +0200
@@ -51,6 +51,7 @@
   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 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 make_list: (key * 'a) list -> 'a list table
   val dest_list: 'a list table -> (key * 'a) list
@@ -374,6 +375,8 @@
 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 insert_list eq (key, x) = default (key, []) #> map_entry key (Library.insert eq x);
+  
 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;