src/Pure/ML/ml_syntax.ML

--- a/src/Pure/ML/ml_syntax.ML	Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Pure/ML/ml_syntax.ML	Fri Sep 20 14:28:13 2024 +0200
@@ -98,7 +98,7 @@
 
 fun print_position pos =
   let val {line, offset, end_offset, props = {label, file, id}} = Position.dest pos in
-    space_implode " "
+    implode_space
       ["Position.make0", print_int line, print_int offset, print_int end_offset,
         print_string label, print_string file, print_string id]
   end;