# HG changeset patch
# User wenzelm
# Date 1729028682 -7200
# Node ID 7c01a86def85e38f3ffab14d35a2502296176a6a
# Parent  98fd5375de00100949d374a79c6b5c7532ab7157
minor performance tuning;

diff -r 98fd5375de00 -r 7c01a86def85 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Tue Oct 15 16:11:37 2024 +0200
+++ b/src/Pure/General/table.ML	Tue Oct 15 23:44:42 2024 +0200
@@ -518,9 +518,7 @@
 (* membership operations *)
 
 fun member eq tab (key, x) =
-  (case lookup tab key of
-    NONE => false
-  | SOME y => eq (x, y));
+  retrieve {result = fn (_, y) => eq (x, y), no_result = false} tab key;
 
 fun insert eq (key, x) =
   modify key (fn NONE => x | SOME y => if eq (x, y) then raise SAME else raise DUP key);
@@ -554,7 +552,7 @@
 
 (* list tables *)
 
-fun lookup_list tab key = these (lookup tab key);
+fun lookup_list tab key = retrieve {result = #2, no_result = []} tab key;
 
 fun cons_list (key, x) tab = modify key (fn NONE => [x] | SOME xs => x :: xs) tab;