# HG changeset patch
# User wenzelm
# Date 1394441641 -3600
# Node ID 8c9ab5d91d5a3c5d011c8d52cabda434b570c093
# Parent  57e2cfba9c6eed8164fa4b28fa590cc98ff4802d
more restrictive completion: intern/extern stability;

diff -r 57e2cfba9c6e -r 8c9ab5d91d5a src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun Mar 09 22:45:09 2014 +0100
+++ b/src/Pure/General/name_space.ML	Mon Mar 10 09:54:01 2014 +0100
@@ -214,7 +214,10 @@
         Symtab.fold
           (fn (a, (name :: _, _)) =>
               if String.isPrefix x a andalso not (is_concealed space name)
-              then cons (ext name, (kind, name)) else I
+              then
+                let val a' = ext name
+                in if a = a' then cons (a', (kind, name)) else I end
+              else I
             | _ => I) internals []
         |> sort_distinct (string_ord o pairself #1);
     in Completion.names pos names end