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