diff -r b90cd7016d4f -r b32aae03e3d6 src/Tools/Code/code_namespace.ML
--- a/src/Tools/Code/code_namespace.ML	Thu Apr 19 08:45:13 2012 +0200
+++ b/src/Tools/Code/code_namespace.ML	Thu Apr 19 10:16:51 2012 +0200
@@ -78,8 +78,8 @@
       end;
     fun add_dependency name name' =
       let
-        val (module_name, base) = dest_name name;
-        val (module_name', base') = dest_name name';
+        val (module_name, _) = dest_name name;
+        val (module_name', _) = dest_name name';
       in if module_name = module_name'
         then (Graph.map_node module_name o apfst) (Graph.add_edge (name, name'))
         else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) name'))
@@ -177,8 +177,8 @@
       end;
     fun add_dependency name name' =
       let
-        val (name_fragments, base) = dest_name name;
-        val (name_fragments', base') = dest_name name';
+        val (name_fragments, _) = dest_name name;
+        val (name_fragments', _) = dest_name name';
         val (name_fragments_common, (diff, diff')) =
           chop_prefix (op =) (name_fragments, name_fragments');
         val is_module = not (null diff andalso null diff');