more compact ML source;

--- 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;
 

--- a/src/Pure/ML/ml_syntax.ML	Sat Oct 21 12:02:23 2023 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Sat Oct 21 14:36:47 2023 +0200
@@ -97,7 +97,11 @@
 val print_properties = print_list (print_pair print_string print_string);
 
 fun print_position pos =
-  "Position.of_properties " ^ print_properties (Position.properties_of pos);
+  let val {line, offset, end_offset, props = {label, file, id}} = Position.dest pos in
+    space_implode " "
+      ["Position.make0", print_int line, print_int offset, print_int end_offset,
+        print_string label, print_string file, print_string id]
+  end;
 
 fun print_range range =
   "Position.range_of_properties " ^ print_properties (Position.properties_of_range range);