src/Pure/ROOT.ML
changeset 59363 4660b0409096
parent 59203 5f0bd5afc16d
child 59470 31d810570879
--- a/src/Pure/ROOT.ML	Tue Jan 13 21:46:09 2015 +0100
+++ b/src/Pure/ROOT.ML	Wed Jan 14 11:52:08 2015 +0100
@@ -65,6 +65,7 @@
 use "General/linear_set.ML";
 use "General/buffer.ML";
 use "General/pretty.ML";
+use "PIDE/xml.ML";
 use "General/path.ML";
 use "General/url.ML";
 use "General/file.ML";
@@ -78,7 +79,6 @@
 if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
 use "General/sha1_samples.ML";
 
-use "PIDE/xml.ML";
 use "PIDE/yxml.ML";
 use "PIDE/document_id.ML";