1.1 --- a/src/Tools/Code/code_namespace.ML	Thu Apr 19 08:45:13 2012 +0200
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Thu Apr 19 10:16:51 2012 +0200
     1.3 @@ -78,8 +78,8 @@
     1.4        end;
     1.5      fun add_dependency name name' =
     1.6        let
     1.7 -        val (module_name, base) = dest_name name;
     1.8 -        val (module_name', base') = dest_name name';
     1.9 +        val (module_name, _) = dest_name name;
    1.10 +        val (module_name', _) = dest_name name';
    1.11        in if module_name = module_name'
    1.12          then (Graph.map_node module_name o apfst) (Graph.add_edge (name, name'))
    1.13          else (Graph.map_node module_name o apsnd) (AList.map_default (op =) (module_name', []) (insert (op =) name'))
    1.14 @@ -177,8 +177,8 @@
    1.15        end;
    1.16      fun add_dependency name name' =
    1.17        let
    1.18 -        val (name_fragments, base) = dest_name name;
    1.19 -        val (name_fragments', base') = dest_name name';
    1.20 +        val (name_fragments, _) = dest_name name;
    1.21 +        val (name_fragments', _) = dest_name name';
    1.22          val (name_fragments_common, (diff, diff')) =
    1.23            chop_prefix (op =) (name_fragments, name_fragments');
    1.24          val is_module = not (null diff andalso null diff');