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