--- a/src/HOL/Import/xml.ML Thu Feb 16 23:31:32 2006 +0100
+++ b/src/HOL/Import/xml.ML Thu Feb 16 23:40:32 2006 +0100
@@ -27,7 +27,7 @@
structure XML :> XML =
struct
-structure Seq = ListScannerSeq
+structure Seq = VectorScannerSeq
structure Scan = Scanner (structure Seq = Seq)
open Scan