# HG changeset patch
# User wenzelm
# Date 1087582062 -7200
# Node ID 9db3d2be8cdf053c50cb258003195417aa010216
# Parent  0343cf20d5680e90c851f76774cb89c5c7149b6c
tuned exists_string;

diff -r 0343cf20d568 -r 9db3d2be8cdf src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Jun 18 20:07:31 2004 +0200
+++ b/src/Pure/library.ML	Fri Jun 18 20:07:42 2004 +0200
@@ -770,10 +770,15 @@
 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
+    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);
+fun exists_string pred str =
+  let
+    val n = size str;
+    fun ex i = i < n andalso (pred (String.substring (str, i, 1)) orelse ex (i + 1));
+  in ex 0 end;
 
 (*enclose in brackets*)
 fun enclose lpar rpar str = lpar ^ str ^ rpar;