tuned -- avoid vacuous reports;

--- a/src/Pure/General/name_space.ML	Sat Mar 15 11:28:07 2014 +0100
+++ b/src/Pure/General/name_space.ML	Sat Mar 15 11:57:55 2014 +0100
@@ -464,9 +464,8 @@
       |> fold (add_name name) accs
       |> new_entry strict (name, (accs', entry));
     val _ =
-      if proper_pos then
-        Context_Position.report_generic context pos
-          (entry_markup true (kind_of space) (name, entry))
+      if proper_pos andalso Context_Position.is_reported_generic context pos then
+        Position.report pos (entry_markup true (kind_of space) (name, entry))
       else ();
   in (name, space') end;