unused (see 696819fe2424);

--- a/src/Pure/PIDE/document.scala	Fri Aug 12 13:16:02 2022 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Aug 12 14:26:17 2022 +0200
@@ -78,9 +78,6 @@
       abbrevs: Thy_Header.Abbrevs = Nil,
       errors: List[String] = Nil
     ) {
-      def imports_offset: Map[Int, Name] =
-        (for { (name, Position.Offset(i)) <- imports_pos } yield i -> name).toMap
-
       def imports: List[Name] = imports_pos.map(_._1)
 
       def append_errors(msgs: List[String]): Header =