src/Pure/General/symbol.scala

--- a/src/Pure/General/symbol.scala	Sun Mar 06 11:59:35 2016 +0100
+++ b/src/Pure/General/symbol.scala	Sun Mar 06 13:19:19 2016 +0100
@@ -54,6 +54,12 @@
   def is_ascii_identifier(s: String): Boolean =
     s.length > 0 && is_ascii_letter(s(0)) && s.forall(is_ascii_letdig)
 
+  def ascii(c: Char): Symbol =
+  {
+    if (c > 127) error("Non-ASCII character: " + quote(c.toString))
+    else char_symbols(c.toInt)
+  }
+
 
   /* symbol matching */