src/Pure/library.ML

--- a/src/Pure/library.ML	Fri May 21 13:07:53 2021 +0200
+++ b/src/Pure/library.ML	Sat May 22 13:35:25 2021 +0200
@@ -132,6 +132,7 @@
   val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
   val exists_string: (string -> bool) -> string -> bool
   val forall_string: (string -> bool) -> string -> bool
+  val member_string: string -> string -> bool
   val first_field: string -> string -> (string * string) option
   val enclose: string -> string -> string -> string
   val unenclose: string -> string
@@ -703,6 +704,8 @@
 
 fun forall_string pred = not o exists_string (not o pred);
 
+fun member_string str s = exists_string (fn s' => s = s') str;
+
 fun first_field sep str =
   let
     val n = size sep;