diff -r df35b5b7b6a4 -r 5286dae99de3 src/Pure/General/vector.ML
--- a/src/Pure/General/vector.ML	Fri Apr 14 22:55:01 2023 +0200
+++ b/src/Pure/General/vector.ML	Sat Apr 15 13:51:38 2023 +0200
@@ -9,6 +9,7 @@
   include VECTOR
   val nth: 'a vector -> int -> 'a
   val forall: ('a -> bool) -> 'a vector -> bool
+  val member: ('a * 'a -> bool) -> 'a vector -> 'a -> bool
   val fold: ('a -> 'b -> 'b) -> 'a vector -> 'b -> 'b
   val fold_rev: ('a -> 'b -> 'b) -> 'a vector -> 'b -> 'b
 end;
@@ -22,6 +23,8 @@
 
 val forall = all;
 
+fun member eq vec x = exists (fn y => eq (x, y)) vec;
+
 fun fold f vec x = foldl (fn (a, b) => f a b) x vec;
 fun fold_rev f vec x = foldr (fn (a, b) => f a b) x vec;