src/Pure/Isar/token.ML
changeset 77779 1f990c8bb74c
parent 77771 279b18bb4059
child 77846 5ba68d3bd741
--- a/src/Pure/Isar/token.ML	Sat Apr 01 15:52:40 2023 +0200
+++ b/src/Pure/Isar/token.ML	Sun Apr 02 12:34:13 2023 +0200
@@ -727,7 +727,7 @@
 
 fun make ((k, n), s) pos =
   let
-    val pos' = Position.advance_offsets n pos;
+    val pos' = Position.shift_offsets {remove_id = false} n pos;
     val range = Position.range (pos, pos');
     val tok =
       if 0 <= k andalso k < Vector.length immediate_kinds then