equal
deleted
inserted
replaced
106 (** string_of_vname **) |
106 (** string_of_vname **) |
107 |
107 |
108 fun string_of_vname (x, i) = |
108 fun string_of_vname (x, i) = |
109 let |
109 let |
110 val si = string_of_int i; |
110 val si = string_of_int i; |
111 val dot = Symbol.is_digit (last_elem (Symbol.explode x)) handle _ => true; |
111 val dot = if_none (try (Symbol.is_digit o last_elem o Symbol.explode) x) true; |
112 in |
112 in |
113 if dot then "?" ^ x ^ "." ^ si |
113 if dot then "?" ^ x ^ "." ^ si |
114 else if i = 0 then "?" ^ x |
114 else if i = 0 then "?" ^ x |
115 else "?" ^ x ^ si |
115 else "?" ^ x ^ si |
116 end; |
116 end; |