diff -r 9473dd79e9c3 -r d3328c562307 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Sat Oct 21 12:02:23 2023 +0200
+++ b/src/Pure/General/position.ML	Sat Oct 21 14:36:47 2023 +0200
@@ -10,6 +10,7 @@
 sig
   eqtype T
   val ord: T ord
+  val make0: int -> int -> int -> string -> string -> string -> T
   val make: Thread_Position.T -> T
   val dest: T -> Thread_Position.T
   val line_of: T -> int option
@@ -78,6 +79,10 @@
 
 datatype T = Pos of Thread_Position.T;
 
+fun make0 line offset end_offset label file id =
+  Pos {line = line, offset = offset, end_offset = end_offset,
+    props = {label = label, file = file, id = id}};
+
 val make = Pos;
 fun dest (Pos args) = args;