minor performance tuning;

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