src/Pure/General/position.ML

--- a/src/Pure/General/position.ML	Sat Apr 01 21:25:24 2023 +0200
+++ b/src/Pure/General/position.ML	Sat Apr 01 21:33:54 2023 +0200
@@ -31,7 +31,6 @@
   val id_only: string -> T
   val put_id: string -> T -> T
   val copy_id: T -> T -> T
-  val id_properties_of: T -> Properties.T
   val parse_id: T -> int option
   val shift_offsets: {remove_id: bool} -> int -> T -> T
   val adjust_offsets: (int -> int option) -> T -> T
@@ -165,11 +164,6 @@
 
 fun parse_id pos = Option.map Value.parse_int (id_of pos);
 
-fun id_properties_of pos =
-  (case id_of pos of
-    SOME id => [(Markup.idN, id)]
-  | NONE => []);
-
 
 (* adjust offsets *)