diff -r 472e48ed9c79 -r 279b18bb4059 src/Pure/General/position.ML --- a/src/Pure/General/position.ML Sat Apr 01 14:32:02 2023 +0200 +++ b/src/Pure/General/position.ML Sat Apr 01 14:50:43 2023 +0200 @@ -35,7 +35,7 @@ val copy_id: T -> T -> T val id_properties_of: T -> Properties.T val parse_id: T -> int option - val advance_offsets: int -> T -> T + val shift_offsets: {remove_id: bool} -> int -> T -> T val adjust_offsets: (int -> int option) -> T -> T val of_properties: Properties.T -> T val properties_of: T -> Properties.T @@ -188,8 +188,6 @@ else Pos {line = line, offset = offset', end_offset = end_offset', props = props'} end; -val advance_offsets = shift_offsets {remove_id = false}; - fun adjust_offsets adjust pos = if is_none (file_of pos) then (case parse_id pos of