src/Pure/General/value.ML

--- a/src/Pure/General/value.ML	Fri Apr 14 20:42:17 2023 +0200
+++ b/src/Pure/General/value.ML	Fri Apr 14 21:34:51 2023 +0200
@@ -42,7 +42,7 @@
 fun parse_int str =
   let
     fun err () = raise Fail ("Bad integer " ^ quote str);
-    fun char i = Char.ord (String.sub (str, i));
+    val char = Char.ord o String.nth str;
     val n = size str;
 
     fun digits i a =