# HG changeset patch
# User wenzelm
# Date 1230809797 -3600
# Node ID 5cf577cb225387fa2db2938ee7606eddc9bcb9ef
# Parent  4588e0070d4c9c01fe80b0188028b508b7df57a0
provide structure CharVector;

diff -r 4588e0070d4c -r 5cf577cb2253 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Thu Jan 01 12:00:36 2009 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Thu Jan 01 12:36:37 2009 +0100
@@ -35,6 +35,7 @@
 load "Process";
 load "FileSys";
 load "IO";
+load "CharVector";
 
 exception Interrupt;