diff -r 3cc55085d490 -r 58e53c61f15f src/Pure/Concurrent/thread_position.ML
--- a/src/Pure/Concurrent/thread_position.ML	Sat Apr 01 19:15:38 2023 +0200
+++ b/src/Pure/Concurrent/thread_position.ML	Sat Apr 01 21:12:44 2023 +0200
@@ -6,7 +6,7 @@
 
 signature THREAD_POSITION =
 sig
-  type T = {line: int, offset: int, end_offset: int, props: (string * string) list}
+  type T = {line: int, offset: int, end_offset: int, props: {file: string, id: string}}
   val none: T
   val get: unit -> T
   val setmp: T -> ('a -> 'b) -> 'a -> 'b
@@ -15,11 +15,11 @@
 structure Thread_Position: THREAD_POSITION =
 struct
 
-type T = {line: int, offset: int, end_offset: int, props: (string * string) list};
+type T = {line: int, offset: int, end_offset: int, props: {file: string, id: string}};
 
 val var = Thread_Data.var () : T Thread_Data.var;
 
-val none: T = {line = 0, offset = 0, end_offset = 0, props = []};
+val none: T = {line = 0, offset = 0, end_offset = 0, props = {file = "", id = ""}};
 
 fun get () = (case Thread_Data.get var of NONE => none | SOME pos => pos);
 fun setmp pos f x = Thread_Data.setmp var (if pos = none then NONE else SOME pos) f x;