--- a/src/Pure/library.ML Fri Apr 14 21:58:22 2023 +0200
+++ b/src/Pure/library.ML Fri Apr 14 22:08:16 2023 +0200
@@ -132,6 +132,7 @@
(*strings*)
val nth_string: string -> int -> string
val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
+ val fold_rev_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
@@ -697,6 +698,8 @@
fun fold_string f = String.fold (f o String.str);
+fun fold_rev_string f = String.fold_rev (f o String.str);
+
fun exists_string pred = String.exists (pred o String.str);
fun forall_string pred = String.forall (pred o String.str);