diff -r fdde1d62e1fb -r 72238ea2201c src/Pure/ML/ml_lex.scala
--- a/src/Pure/ML/ml_lex.scala	Sat Feb 15 16:49:10 2014 +0100
+++ b/src/Pure/ML/ml_lex.scala	Sat Feb 15 16:55:48 2014 +0100
@@ -68,6 +68,7 @@
       repeated(character(Symbol.is_ascii_digit), 3, 3)
 
     private val str =
+      one(Symbol.is_symbolic) |
       one(character(c => c != '"' && c != '\\' && ' ' <= c && c <= '~')) |
       "\\" ~ escape ^^ { case x ~ y => x + y }