src/HOL/Import/mono_scan.ML
changeset 40627 becf5d5187cc
parent 32960 69916a850301
child 41589 bbd861837ebc
     1.1 --- a/src/HOL/Import/mono_scan.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/HOL/Import/mono_scan.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -233,6 +233,6 @@
     1.4  fun this [] = (fn toks => ([], toks))
     1.5    | this (xs' as (x::xs)) = one (fn y => x=y) -- this xs >> K xs'
     1.6  
     1.7 -fun this_string s = this (explode s) >> K s
     1.8 +fun this_string s = this (raw_explode s) >> K s
     1.9  
    1.10  end
    1.11 \ No newline at end of file