src/HOL/Import/lazy_seq.ML
changeset 40627 becf5d5187cc
parent 33339 d41f77196338
     1.1 --- a/src/HOL/Import/lazy_seq.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/HOL/Import/lazy_seq.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -543,7 +543,7 @@
     1.4          F e (getItem s)
     1.5      end
     1.6  
     1.7 -fun fromString s = of_list (explode s)
     1.8 +fun fromString s = of_list (raw_explode s)
     1.9  
    1.10  end
    1.11