# HG changeset patch
# User obua
# Date 1140129632 -3600
# Node ID a6a15d3446ad486744247c5c17a852aed14b1dc4
# Parent  c442f3362f7ad1ff85ec32c576c9369021ee9667
use VectorScannerSeq instead of ListScannerSeq in xml.ML

diff -r c442f3362f7a -r a6a15d3446ad src/HOL/Import/xml.ML
--- 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