# HG changeset patch
# User wenzelm
# Date 1681502302 -7200
# Node ID ba563d3f73ff79cc395c113c0e906eb0ee03dd11
# Parent  d73451fb71623e14bdbc6912cdf6423b09be2e2c
tuned: more direct re-use;

diff -r d73451fb7162 -r ba563d3f73ff src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Apr 14 21:39:10 2023 +0200
+++ b/src/Pure/library.ML	Fri Apr 14 21:58:22 2023 +0200
@@ -693,22 +693,13 @@
 
 (* functions tuned for strings, avoiding explode *)
 
-fun nth_string str i = String.substring (str, i, 1);
+fun nth_string str = String.str o String.nth str;
+
+fun fold_string f = String.fold (f o String.str);
 
-fun fold_string f str x0 =
-  let
-    val n = size str;
-    fun iter (x, i) =
-      if i < n then iter (f (String.substring (str, i, 1)) x, i + 1) else x;
-  in iter (x0, 0) end;
+fun exists_string pred = String.exists (pred o String.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;
-
-fun forall_string pred = not o exists_string (not o pred);
+fun forall_string pred = String.forall (pred o String.str);
 
 fun member_string str s = exists_string (fn s' => s = s') str;