equal
deleted
inserted
replaced
81 |
81 |
82 structure Table = Table(type key = T val ord = symbol_ord); |
82 structure Table = Table(type key = T val ord = symbol_ord); |
83 structure Graph = Graph(type key = T val ord = symbol_ord); |
83 structure Graph = Graph(type key = T val ord = symbol_ord); |
84 |
84 |
85 local |
85 local |
86 val base = Name.desymbolize false o Long_Name.base_name; |
86 val base = Name.desymbolize (SOME false) o Long_Name.base_name; |
87 fun base_rel (x, y) = base y ^ "_" ^ base x; |
87 fun base_rel (x, y) = base y ^ "_" ^ base x; |
88 in |
88 in |
89 |
89 |
90 fun default_base (Constant "") = "value" |
90 fun default_base (Constant "") = "value" |
91 | default_base (Constant c) = base c |
91 | default_base (Constant c) = base c |