src/Pure/General/name_space.ML
changeset 55696 de2668c50403
parent 55694 a1184dfb8e00
child 55742 a989bdaf8121
--- a/src/Pure/General/name_space.ML	Sun Feb 23 21:30:35 2014 +0100
+++ b/src/Pure/General/name_space.ML	Sun Feb 23 21:30:47 2014 +0100
@@ -447,7 +447,9 @@
 fun check context (space, tab) (xname, pos) =
   let val name = intern space xname in
     (case Symtab.lookup tab name of
-      SOME x => (Context_Position.report_generic context pos (markup space name); (name, x))
+      SOME x =>
+       (Context_Position.report_generic context pos (markup space name);
+        (name, x))
     | NONE =>
        (Completion.report (completion context space (xname, pos));
         error (undefined (kind_of space) name ^ Position.here pos)))