src/Pure/name.ML

--- a/src/Pure/name.ML	Fri Apr 14 16:01:00 2023 +0200
+++ b/src/Pure/name.ML	Fri Apr 14 20:42:17 2023 +0200
@@ -59,8 +59,8 @@
   in ":" ^ leading ^ string_of_int i end);
 
 fun bound n =
-  if n < 1000 then Vector.sub (small_int, n)
-  else ":" ^ bound (n div 1000) ^ Vector.sub (small_int, n mod 1000);
+  if n < 1000 then Vector.nth small_int n
+  else ":" ^ bound (n div 1000) ^ Vector.nth small_int (n mod 1000);
 
 val is_bound = String.isPrefix ":";