changeset 40627 | becf5d5187cc |
parent 34307 | 9074aa7d06e0 |
child 42357 | 3305f573294e |
--- a/src/Pure/name.ML Fri Nov 19 23:48:07 2010 +0100 +++ b/src/Pure/name.ML Sat Nov 20 00:53:26 2010 +0100 @@ -166,7 +166,7 @@ if is_valid x then x :: xs else (case Symbol.decode x of - Symbol.Sym name => "_" :: explode name @ sep xs + Symbol.Sym name => "_" :: raw_explode name @ sep xs | _ => sep xs); fun upper_lower cs = if upper then nth_map 0 Symbol.to_ascii_upper cs