src/Pure/library.ML

--- a/src/Pure/library.ML	Tue Jun 21 16:03:00 2022 +0200
+++ b/src/Pure/library.ML	Tue Jun 21 22:17:11 2022 +0200
@@ -135,6 +135,7 @@
   val exists_string: (string -> bool) -> string -> bool
   val forall_string: (string -> bool) -> string -> bool
   val member_string: string -> string -> bool
+  val last_string: string -> string option
   val first_field: string -> string -> (string * string) option
   val enclose: string -> string -> string -> string
   val unenclose: string -> string
@@ -714,6 +715,9 @@
 
 fun member_string str s = exists_string (fn s' => s = s') str;
 
+fun last_string "" = NONE
+  | last_string s = SOME (str (String.sub (s, size s - 1)));
+
 fun first_field sep str =
   let
     val n = size sep;