src/Pure/General/name_space.ML
changeset 55977 ec4830499634
parent 55975 9962ca0875c9
child 55989 55827fc7c0dd
--- a/src/Pure/General/name_space.ML	Fri Mar 07 13:29:10 2014 +0100
+++ b/src/Pure/General/name_space.ML	Fri Mar 07 14:37:25 2014 +0100
@@ -214,7 +214,7 @@
         Symtab.fold
           (fn (a, (name :: _, _)) =>
               if String.isPrefix x a andalso not (is_concealed space name)
-              then cons (ext name, Long_Name.implode [kind, name]) else I
+              then cons (ext name, (kind, name)) else I
             | _ => I) internals []
         |> sort_distinct (string_ord o pairself #1);
     in Completion.names pos names end