diff -r 19b77b1de188 -r 5f1f0a20af4d src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Wed Jun 10 11:28:39 2009 +0200
+++ b/src/Pure/General/symbol.scala	Wed Jun 10 11:29:57 2009 +0200
@@ -20,12 +20,12 @@
     [^\\ \ud800-\udfff] | [\ud800-\udbff][\udc00-\udfff] """)
 
   private val symbol = new Regex("""(?xs)
-      \\ \\? < (?:
+      \\ < (?:
       \^? [A-Za-z][A-Za-z0-9_']* |
       \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* ) >""")
 
   private val bad_symbol = new Regex("(?xs) (?!" + symbol + ")" +
-    """ \\ \\? < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
+    """ \\ < (?: (?! \s | [\"`\\] | \(\* | \*\) | \{\* | \*\} ) . )*""")
 
   // total pattern
   val regex = new Regex(plain + "|" + symbol + "|" + bad_symbol + "| .")
@@ -133,7 +133,7 @@
             }
           val ch = new String(Character.toChars(code))
         } yield (sym, ch)
-      (new Recoder(mapping ++ (for ((x, y) <- mapping) yield ("\\" + x, y))),
+      (new Recoder(mapping),
        new Recoder(for ((x, y) <- mapping) yield (y, x)))
     }