foldl_string;

--- a/src/Pure/library.ML	Fri Feb 12 14:40:56 1999 +0100
+++ b/src/Pure/library.ML	Sat Feb 13 22:08:54 1999 +0100
@@ -122,6 +122,7 @@
   val string_of_indexname: string * int -> string
 
   (*strings*)
+  val foldl_string: ('a * string -> 'a) -> 'a * string -> 'a
   val enclose: string -> string -> string -> string
   val quote: string -> string
   val space_implode: string -> string list -> string
@@ -652,6 +653,13 @@
 
 (** strings **)
 
+(*tuned version of foldl for strings, avoids explode*)
+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;
+
 (*enclose in brackets*)
 fun enclose lpar rpar str = lpar ^ str ^ rpar;