# HG changeset patch
# User wenzelm
# Date 1459529185 -7200
# Node ID 5f73bf6ba98bcddd52997a5119f5ea82a8e83cb1
# Parent  ddc58826cbe958db618dfb7949d60ea59f631f3f
required space is already part of Position.here;

diff -r ddc58826cbe9 -r 5f73bf6ba98b src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Fri Apr 01 18:43:54 2016 +0200
+++ b/src/Pure/General/position.ML	Fri Apr 01 18:46:25 2016 +0200
@@ -214,7 +214,7 @@
     else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
   end;
 
-val here_list = space_implode " " o map here;
+val here_list = implode o map here;
 
 
 (* range *)