src/Tools/Code/code_printer.ML
changeset 40875 becf5d5187cc
parent 39902 d9fb92a8c80a
child 44206 2b47822868e4
     1.1 --- a/src/Tools/Code/code_printer.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/Tools/Code/code_printer.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -173,8 +173,8 @@
     1.4   of SOME name' => name'
     1.5    | NONE => error ("Invalid name in context: " ^ quote name);
     1.6  
     1.7 -val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
     1.8 -val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
     1.9 +val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o raw_explode;
    1.10 +val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o raw_explode;
    1.11  
    1.12  fun aux_params vars lhss =
    1.13    let