src/HOL/Import/mono_scan.ML

--- a/src/HOL/Import/mono_scan.ML	Fri Nov 19 23:48:07 2010 +0100
+++ b/src/HOL/Import/mono_scan.ML	Sat Nov 20 00:53:26 2010 +0100
@@ -233,6 +233,6 @@
 fun this [] = (fn toks => ([], toks))
   | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
 
-fun this_string s = this (explode s) >> K s
+fun this_string s = this (raw_explode s) >> K s
 
 end
\ No newline at end of file