--- a/src/Pure/General/name_space.ML Mon Jun 06 08:13:07 2016 +0200
+++ b/src/Pure/General/name_space.ML Mon Jun 06 08:36:03 2016 +0200
@@ -269,9 +269,9 @@
val ext = extern_shortest (Context.proof_of context) space;
in
Change_Table.fold
- (fn (a, (name :: _, _)) =>
- if completed a andalso not (is_concealed space name) then
- cons (a = ext name, (a, (kind, name)))
+ (fn (xname', (name :: _, _)) =>
+ if completed xname' andalso not (is_concealed space name) then
+ cons (xname' = ext name, (xname', (kind, name)))
else I
| _ => I) internals []
|> sort_distinct result_ord