src/HOL/Import/seq.ML
changeset 40627 becf5d5187cc
parent 32960 69916a850301
     1.1 --- a/src/HOL/Import/seq.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/HOL/Import/seq.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -94,6 +94,6 @@
     1.4  open Extended
     1.5  
     1.6  val fromList = I
     1.7 -val fromString = explode
     1.8 +val fromString = raw_explode
     1.9  
    1.10  end