# HG changeset patch
# User obua
# Date 1140185006 -3600
# Node ID 9497f7b174bed78729c9f0f468a52ccfa53e7d9d
# Parent  968e95fdbf8a095d53337ad81f7ffb98736332f6
replaced Symbol.explode by explode

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
 
diff -r 968e95fdbf8a -r 9497f7b174be src/HOL/Import/seq.ML
--- 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
diff -r 968e95fdbf8a -r 9497f7b174be src/HOL/Import/xml.ML
--- 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) **)