src/Pure/Isar/token.ML

--- a/src/Pure/Isar/token.ML	Fri Apr 14 16:01:00 2023 +0200
+++ b/src/Pure/Isar/token.ML	Fri Apr 14 20:42:17 2023 +0200
@@ -731,7 +731,7 @@
     val range = Position.range (pos, pos');
     val tok =
       if 0 <= k andalso k < Vector.length immediate_kinds then
-        Token ((s, range), (Vector.sub (immediate_kinds, k), s), Slot)
+        Token ((s, range), (Vector.nth immediate_kinds k, s), Slot)
       else
         (case explode Keyword.empty_keywords pos s of
           [tok] => tok