src/HOL/Import/xml.ML
changeset 19091 a6a15d3446ad
parent 19089 2e487fe9593a
child 19093 6d584f9d2021
--- 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