clarified signature;

--- a/src/Pure/General/position.ML	Sat Apr 01 13:58:45 2023 +0200
+++ b/src/Pure/General/position.ML	Sat Apr 01 14:32:02 2023 +0200
@@ -39,7 +39,6 @@
   val adjust_offsets: (int -> int option) -> T -> T
   val of_properties: Properties.T -> T
   val properties_of: T -> Properties.T
-  val offset_properties_of: T -> Properties.T
   val def_properties_of: T -> Properties.T
   val entity_markup: string -> string * T -> Markup.T
   val make_entity_markup: {def: bool} -> serial -> string -> string * T -> Markup.T
@@ -223,10 +222,6 @@
   int_entry Markup.offsetN offset @
   int_entry Markup.end_offsetN end_offset @ props;
 
-fun offset_properties_of (Pos {offset, end_offset, ...}) =
-  int_entry Markup.offsetN offset @
-  int_entry Markup.end_offsetN end_offset;
-
 val def_properties_of = properties_of #> map (apfst Markup.def_name);
 
 fun entity_markup kind (name, pos) =

--- a/src/Pure/Thy/thy_info.ML	Sat Apr 01 13:58:45 2023 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sat Apr 01 14:32:02 2023 +0200
@@ -39,8 +39,13 @@
     segments: Document_Output.segment list};
 
 fun adjust_pos_properties (context: presentation_context) pos =
-  Position.offset_properties_of (#adjust_pos context pos) @
-  filter (fn (a, _) => a = Markup.idN orelse a = Markup.fileN) (Position.get_props pos);
+  let
+    val props = Position.properties_of pos;
+    val props' = Position.properties_of (#adjust_pos context pos);
+  in
+    filter (fn (a, _) => a = Markup.offsetN orelse a = Markup.end_offsetN) props' @
+    filter (fn (a, _) => a = Markup.idN orelse a = Markup.fileN) props
+  end;
 
 structure Presentation = Theory_Data
 (