src/Pure/General/scan.ML

--- a/src/Pure/General/scan.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/Pure/General/scan.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -154,7 +154,7 @@
           if (y: string) = x then drop_prefix ys xs else raise FAIL NONE;
   in (ys, drop_prefix ys xs) end;
 
-fun this_string s = this (explode s) >> K s;  (*primitive string -- no symbols here!*)
+fun this_string s = this (raw_explode s) >> K s;  (*primitive string -- no symbols here!*)
 
 fun many _ [] = raise MORE NONE
   | many pred (lst as x :: xs) =