# HG changeset patch
# User wenzelm
# Date 1681502896 -7200
# Node ID d589d1d218b25f6b11539252da589bd1eb558344
# Parent  ba563d3f73ff79cc395c113c0e906eb0ee03dd11
more operations;

diff -r ba563d3f73ff -r d589d1d218b2 src/Pure/library.ML
--- 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);