diff -r 15652e058e28 -r d361b0a99e31 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Mar 09 12:06:09 1999 +0100
+++ b/src/Pure/library.ML	Tue Mar 09 12:07:16 1999 +0100
@@ -122,7 +122,9 @@
   val string_of_indexname: string * int -> string
 
   (*strings*)
+  val nth_elem_string: int * string -> string
   val foldl_string: ('a * string -> 'a) -> 'a * string -> 'a
+  val exists_string: (string -> bool) -> string -> bool
   val enclose: string -> string -> string -> string
   val quote: string -> string
   val space_implode: string -> string list -> string
@@ -653,13 +655,19 @@
 
 (** strings **)
 
-(*tuned version of foldl for strings, avoids explode*)
+(*functions tuned for strings, avoiding explode*)
+
+fun nth_elem_string (i, str) =
+  String.substring (str, i, 1) handle _ => raise LIST "nth_elem_string";
+
 fun foldl_string f (x0, str) =
   let
     val n = size str;
     fun fold (x, i) = if i < n then fold (f (x, String.substring (str, i, 1)), i + 1) else x
   in fold (x0, 0) end;
 
+fun exists_string pred str = foldl_string (fn (b, s) => b orelse pred s) (false, str);
+
 (*enclose in brackets*)
 fun enclose lpar rpar str = lpar ^ str ^ rpar;