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