diff -r c2a41f31cacb -r 85463aff6dbe src/Tools/code/code_target.ML
--- a/src/Tools/code/code_target.ML	Mon Oct 22 16:54:52 2007 +0200
+++ b/src/Tools/code/code_target.ML	Mon Oct 22 16:54:54 2007 +0200
@@ -1394,7 +1394,7 @@
     fun add_def (name, (def, deps)) =
       let
         val (modl, base) = dest_name name;
-        fun name_def base = Name.variants [base] #>> the_single;
+        val name_def = yield_singleton Name.variants;
         fun add_fun upper (nsp_fun, nsp_typ) =
           let
             val (base', nsp_fun') =
@@ -1490,6 +1490,7 @@
           |> remove (op =) modlname';
         val qualified =
           imports @ map fst defs
+          |> distinct (op =)
           |> map_filter (try deresolv)
           |> map NameSpace.base
           |> has_duplicates (op =);