# HG changeset patch
# User wenzelm
# Date 1465202096 -7200
# Node ID 7238ed9a27ab0183306fc524aef8530f0c0dc39c
# Parent  54197a7c1bbddf1ef9374d23084cd76081eb68fb
less redundant exploration of full name space;

diff -r 54197a7c1bbd -r 7238ed9a27ab src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Jun 06 08:36:03 2016 +0200
+++ b/src/Pure/General/name_space.ML	Mon Jun 06 10:34:56 2016 +0200
@@ -267,12 +267,16 @@
         | ord => ord);
       val Name_Space {kind, internals, ...} = space;
       val ext = extern_shortest (Context.proof_of context) space;
+      val full = Name.clean xname = "";
     in
       Change_Table.fold
         (fn (xname', (name :: _, _)) =>
-            if completed xname' andalso not (is_concealed space name) then
-              cons (xname' = ext name, (xname', (kind, name)))
-            else I
+              if completed xname' andalso not (is_concealed space name) then
+                let val xname'' = ext name in
+                  if xname' <> xname'' andalso full then I
+                  else cons (xname' = xname'', (xname', (kind, name)))
+                end
+              else I
           | _ => I) internals []
       |> sort_distinct result_ord
       |> map #2