diff -r 4ccfe99c160b -r b66639331db5 src/Tools/Code/code_symbol.ML
--- a/src/Tools/Code/code_symbol.ML	Thu May 01 09:30:34 2014 +0200
+++ b/src/Tools/Code/code_symbol.ML	Thu May 01 09:30:35 2014 +0200
@@ -83,7 +83,7 @@
 structure Graph = Graph(type key = T val ord = symbol_ord);
 
 local
-  val base = Name.desymbolize false o Long_Name.base_name;
+  val base = Name.desymbolize (SOME false) o Long_Name.base_name;
   fun base_rel (x, y) = base y ^ "_" ^ base x;
 in