changeset 55957 | cffb46aea3d1 |
parent 55956 | 94d384d621b0 |
child 55961 | c2d4a3608441 |
--- a/src/Pure/General/name_space.ML Thu Mar 06 16:12:26 2014 +0100 +++ b/src/Pure/General/name_space.ML Thu Mar 06 16:24:47 2014 +0100 @@ -460,7 +460,7 @@ val completions = map (fn pos => completion context space (xname, pos)) ps; in error (undefined (kind_of space) name ^ Position.here_list ps ^ - implode (map (Markup.markup_report o Completion.reported_text) completions)) + Markup.markup_report (implode (map Completion.reported_text completions))) end) end;