# HG changeset patch
# User wenzelm
# Date 1499068646 -7200
# Node ID 8d966b4a7469233d1c894bafb04a04f1cf650eaa
# Parent  c2c18b6b48daff696c2282e73165318de6987647
tuned;

diff -r c2c18b6b48da -r 8d966b4a7469 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Jul 03 09:20:24 2017 +0200
+++ b/src/Pure/General/name_space.ML	Mon Jul 03 09:57:26 2017 +0200
@@ -271,15 +271,17 @@
       val Name_Space {kind, internals, ...} = space;
       val ext = extern_shortest (Context.proof_of context) space;
       val full = Name.clean xname = "";
+
+      fun complete_external xname' name =
+        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;
     in
       Change_Table.fold
-        (fn (xname', (name :: _, _)) =>
-              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
+        (fn (xname', (name :: _, _)) => complete_external xname' name
           | _ => I) internals []
       |> sort_distinct result_ord
       |> map #2