src/Pure/General/name_space.ML

   else
     let val names = valid_accesses space name in
       space
       |> add_name' name name
       |> fold (del_name name)
-        (if fully then names else names inter_string [Long_Name.base_name name])
+        (if fully then names else gen_inter (op =) (names, [Long_Name.base_name name]))
       |> fold (del_name_extra name) (get_accesses space name)
     end;
 
 
 (* merge *)