src/Pure/ROOT.ML
changeset 59363 4660b0409096
parent 59203 5f0bd5afc16d
child 59470 31d810570879
     1.1 --- a/src/Pure/ROOT.ML	Tue Jan 13 21:46:09 2015 +0100
     1.2 +++ b/src/Pure/ROOT.ML	Wed Jan 14 11:52:08 2015 +0100
     1.3 @@ -65,6 +65,7 @@
     1.4  use "General/linear_set.ML";
     1.5  use "General/buffer.ML";
     1.6  use "General/pretty.ML";
     1.7 +use "PIDE/xml.ML";
     1.8  use "General/path.ML";
     1.9  use "General/url.ML";
    1.10  use "General/file.ML";
    1.11 @@ -78,7 +79,6 @@
    1.12  if ML_System.is_polyml then use "General/sha1_polyml.ML" else ();
    1.13  use "General/sha1_samples.ML";
    1.14  
    1.15 -use "PIDE/xml.ML";
    1.16  use "PIDE/yxml.ML";
    1.17  use "PIDE/document_id.ML";
    1.18