changeset 40627 | becf5d5187cc |
parent 39148 | b6530978c14d |
child 41100 | 6c0940392fb4 |
--- a/src/Tools/Code/code_ml.ML Fri Nov 19 23:48:07 2010 +0100 +++ b/src/Tools/Code/code_ml.ML Sat Nov 20 00:53:26 2010 +0100 @@ -679,7 +679,7 @@ fun chr i = let val xs = string_of_int i; - val ys = replicate_string (3 - length (explode xs)) "0"; + val ys = replicate_string (3 - length (raw_explode xs)) "0"; in "\\" ^ ys ^ xs end; fun char_ocaml c = let