--- 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