--- 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