diff -r ec2b50aeb0dd -r 1f93e376aeb6 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Wed Oct 25 14:39:22 2017 +0200
+++ b/src/Pure/General/symbol.scala	Wed Oct 25 14:54:28 2017 +0200
@@ -60,6 +60,8 @@
     else char_symbols(c.toInt)
   }
 
+  def is_ascii(s: Symbol): Boolean = s.length == 1 && s(0) < 128
+
 
   /* symbol matching */