src/Pure/General/name_space.ML
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;