# HG changeset patch
# User wenzelm
# Date 1152790925 -7200
# Node ID caf3a129b90d103767b93e51d455a8b2d3abafda
# Parent  88fa4127382471c2a218280e6f2be6fa07b49ea3
tuned insert_list;

diff -r 88fa41273824 -r caf3a129b90d src/Pure/General/table.ML
--- 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