author | wenzelm |
Mon, 10 Mar 2014 09:54:01 +0100 | |
changeset 56022 | 8c9ab5d91d5a |
parent 56015 | 57e2cfba9c6e |
child 56023 | f252a315c26e |
--- 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