--- 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');