| changeset 62803 | 5f73bf6ba98b |
| parent 62800 | 7ac100f86863 |
| child 62889 | 99c7f31615c2 |
--- 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 *)