src/Pure/library.ML

   (*strings*)
   val nth_string: string -> int -> string
   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
   val quote: string -> string
   val cartouche: string -> string

     fun ex i = i < n andalso (pred (String.substring (str, i, 1)) orelse ex (i + 1));
   in ex 0 end;
 
 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;
     val len = size str;
     fun find i =