src/Pure/ML/ml_lex.ML

--- a/src/Pure/ML/ml_lex.ML	Mon Dec 08 15:21:57 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Mon Dec 08 15:59:30 2014 +0100
@@ -295,7 +295,10 @@
 
 fun gen_read SML pos text =
   let
-    val syms = Symbol_Pos.explode (text, pos);
+    val syms =
+      Symbol_Pos.explode (text, pos)
+      |> SML ? maps (fn (s, p) => raw_explode s |> map (rpair p));
+
     val termination =
       if null syms then []
       else