src/Pure/codegen.ML
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