tuned insert_list;

--- a/src/Pure/General/table.ML	Thu Jul 13 13:42:02 2006 +0200
+++ b/src/Pure/General/table.ML	Thu Jul 13 13:42:05 2006 +0200
@@ -375,7 +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 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