--- a/src/HOL/Import/seq.ML	Fri Feb 17 08:42:41 2006 +0100
+++ b/src/HOL/Import/seq.ML	Fri Feb 17 15:03:26 2006 +0100
@@ -94,6 +94,6 @@
 open Extended
 
 val fromList = I
-val fromString = Symbol.explode
+val fromString = explode
 
 end
changeset 19095	9497f7b174be
parent 19089	2e487fe9593a
child 32960	69916a850301