| 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