src/Pure/General/position.ML

   in
     if s2 = "" then ""
     else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
   end;
 
-val here_list = implode o map here;
+val here_list = map here #> distinct (op =) #> implode;
 
 
 (* range *)
 
 type range = T * T;