# HG changeset patch
# User berghofe
# Date 1011620867 -3600
# Node ID cdf586d56b8a1ac9c2e9c485dc240dcb3696f241
# Parent  9d3f5056296b78bc8a7d126a6b1ffb7bf1de0551
Tuned name mangling function.

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