# HG changeset patch
# User wenzelm
# Date 1465194963 -7200
# Node ID 54197a7c1bbddf1ef9374d23084cd76081eb68fb
# Parent  ae5275fa96dcc578d6bb63c5d55ae2a217144793
tuned;

diff -r ae5275fa96dc -r 54197a7c1bbd src/Pure/General/name_space.ML
--- 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