--- a/src/Pure/General/name_space.ML Mon Nov 12 14:02:33 2018 +0100
+++ b/src/Pure/General/name_space.ML Mon Nov 12 15:14:12 2018 +0100
@@ -564,12 +564,9 @@
|> map (fn pos => (pos, markup space name));
in ((name, reports), x) end
| NONE =>
- let
- val completions = map (fn pos => completion context space (K true) (xname, pos)) ps;
- in
- error (undefined space name ^ Position.here_list ps ^
- Markup.markup_report (implode (map Completion.reported_text completions)))
- end)
+ error (undefined space name ^ Position.here_list ps ^
+ Completion.markup_report
+ (map (fn pos => completion context space (K true) (xname, pos)) ps)))
end;
fun check context table (xname, pos) =