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

diff -r a12c48fbf10f -r 2585ce904bb3 src/Pure/library.ML
--- a/src/Pure/library.ML	Sat May 06 23:20:20 2023 +0200
+++ b/src/Pure/library.ML	Sun May 07 12:24:37 2023 +0200
@@ -836,7 +836,13 @@
 
 fun insert eq x xs = if member eq xs x then xs else x :: xs;
 fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs;
-fun update eq x xs = cons x (remove eq x xs);
+
+fun update eq x list =
+  (case list of
+    [] => [x]
+  | y :: rest =>
+      if member eq rest x then x :: remove eq x list
+      else if eq (x, y) then list else x :: list);
 
 fun inter eq xs = filter (member eq xs);