replaced Symbol.explode by explode

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

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

--- a/src/HOL/Import/xml.ML	Fri Feb 17 08:42:41 2006 +0100
+++ b/src/HOL/Import/xml.ML	Fri Feb 17 15:03:26 2006 +0100
@@ -32,6 +32,7 @@
 structure Seq = StringScannerSeq
 structure Scan = StringScanner
 
+
 open Scan
 
 (** string based representation (small scale) **)