src/Pure/ROOT.ML
changeset 44698 0385292321a0
parent 44549 5e5e6ad3922c
child 45026 5c0b0d67f9b1
--- a/src/Pure/ROOT.ML	Sun Sep 04 14:29:15 2011 +0200
+++ b/src/Pure/ROOT.ML	Sun Sep 04 15:21:50 2011 +0200
@@ -54,17 +54,18 @@
 use "General/linear_set.ML";
 use "General/buffer.ML";
 use "General/pretty.ML";
-use "General/xml.ML";
 use "General/path.ML";
 use "General/url.ML";
 use "General/file.ML";
-use "General/yxml.ML";
 use "General/long_name.ML";
 use "General/binding.ML";
 
 use "General/sha1.ML";
 if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
 
+use "PIDE/xml.ML";
+use "PIDE/yxml.ML";
+
 
 (* concurrency within the ML runtime *)