diff -r 48429ad6d0c8 -r 50ccc027e8a7 src/Pure/ML/ml_lex.scala
--- a/src/Pure/ML/ml_lex.scala	Mon Dec 08 11:49:04 2014 +0100
+++ b/src/Pure/ML/ml_lex.scala	Mon Dec 08 11:50:04 2014 +0100
@@ -90,8 +90,8 @@
       repeated(character(Symbol.is_ascii_digit), 3, 3)
 
     private val str =
-      one(Symbol.is_symbolic) |
       one(character(c => c != '"' && c != '\\' && ' ' <= c && c <= '~')) |
+      one(s => Symbol.is_symbolic(s) | Symbol.is_control(s)) |
       "\\" ~ escape ^^ { case x ~ y => x + y }