author | wenzelm |
Sat, 08 Dec 2001 14:42:22 +0100 | |
changeset 12420 | a2a05c952b4d |
parent 12419 | 6a7ee57447aa |
child 12421 | 54c06c1f88b8 |
1.1 --- a/src/Pure/General/ROOT.ML Sat Dec 08 14:42:03 2001 +0100 1.2 +++ b/src/Pure/General/ROOT.ML Sat Dec 08 14:42:22 2001 +0100 1.3 @@ -20,6 +20,7 @@ 1.4 use "buffer.ML"; 1.5 use "history.ML"; 1.6 use "pretty.ML"; 1.7 +use "xml.ML"; 1.8 1.9 structure PureGeneral = 1.10 struct 1.11 @@ -38,4 +39,5 @@ 1.12 structure Buffer = Buffer; 1.13 structure History = History; 1.14 structure Pretty = Pretty; 1.15 + structure XML = XML; 1.16 end;