diff -r 968e95fdbf8a -r 9497f7b174be src/HOL/Import/lazy_seq.ML
--- a/src/HOL/Import/lazy_seq.ML	Fri Feb 17 08:42:41 2006 +0100
+++ b/src/HOL/Import/lazy_seq.ML	Fri Feb 17 15:03:26 2006 +0100
@@ -546,7 +546,7 @@
 	F e (getItem s)
     end
 
-fun fromString s = of_list (Symbol.explode s)
+fun fromString s = of_list (explode s)
 
 end