--- 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