changeset 12824 | cdf586d56b8a |
parent 12580 | 7fdc00bb2a9e |
child 13003 | 3d5807d45439 |
--- a/src/Pure/codegen.ML Mon Jan 21 14:45:00 2002 +0100 +++ b/src/Pure/codegen.ML Mon Jan 21 14:47:47 2002 +0100 @@ -242,7 +242,7 @@ fun check_str [] = "" | check_str (" " :: xs) = "_" ^ check_str xs | check_str (x :: xs) = - (if Symbol.is_letter x orelse Symbol.is_digit x orelse x="_" then x + (if Symbol.is_letdig x then x else "_" ^ string_of_int (ord x)) ^ check_str xs in (if not (Symbol.is_letter x) then "id" else "") ^ check_str xs