changeset 56811 | b66639331db5 |
parent 56810 | 4ccfe99c160b |
child 56826 | ba18bd41e510 |
--- 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