# HG changeset patch
# User wenzelm
# Date 1683455411 -7200
# Node ID f83702560730990e701aa10864f7fd8d8767d478
# Parent  2585ce904bb30a6fabf16adbc30272217bec514a
minor performance tuning;

diff -r 2585ce904bb3 -r f83702560730 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sun May 07 12:24:37 2023 +0200
+++ b/src/Pure/General/table.ML	Sun May 07 12:30:11 2023 +0200
@@ -56,8 +56,8 @@
   val lookup_list: 'a list table -> key -> 'a list
   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 update_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) -> 'a list table * 'a list table -> 'a list table
@@ -621,17 +621,23 @@
 
 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 modify_list key f =
+  modify key (fn arg =>
+    let
+      val xs = the_default [] arg;
+      val ys = f xs;
+    in if pointer_eq (xs, ys) then raise SAME else ys end);
+
+fun insert_list eq (key, x) = modify_list key (Library.insert eq x);
+fun update_list eq (key, x) = modify_list key (Library.update 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
+  map_entry key (fn xs =>
+    (case Library.remove eq x xs of
+      [] => raise UNDEF key
+    | ys => if pointer_eq (xs, ys) then raise SAME else ys)) tab
   handle UNDEF _ => delete key tab;
 
-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 = build (fold_rev cons_list args);
 fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab);
 fun merge_list eq =