diff -r 9d3f5056296b -r cdf586d56b8a src/Pure/codegen.ML
--- 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