src/Pure/General/scan.ML
changeset 40627 becf5d5187cc
parent 38875 c7a66b584147
child 43947 9b00f09f7721
     1.1 --- a/src/Pure/General/scan.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/Pure/General/scan.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -154,7 +154,7 @@
     1.4            if (y: string) = x then drop_prefix ys xs else raise FAIL NONE;
     1.5    in (ys, drop_prefix ys xs) end;
     1.6  
     1.7 -fun this_string s = this (explode s) >> K s;  (*primitive string -- no symbols here!*)
     1.8 +fun this_string s = this (raw_explode s) >> K s;  (*primitive string -- no symbols here!*)
     1.9  
    1.10  fun many _ [] = raise MORE NONE
    1.11    | many pred (lst as x :: xs) =