tuned;

--- a/src/Pure/library.ML	Sun Apr 23 19:51:46 2023 +0200
+++ b/src/Pure/library.ML	Sun Apr 23 19:57:40 2023 +0200
@@ -820,9 +820,9 @@
 
 fun member eq list x =
   let
-    fun memb [] = false
-      | memb (y :: ys) = eq (x, y) orelse memb ys;
-  in memb list end;
+    fun mem [] = false
+      | mem (y :: ys) = eq (x, y) orelse mem ys;
+  in mem list end;
 
 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;