src/Pure/ROOT.ML
changeset 70784 799437173553
parent 70574 503ca64329cc
child 70893 ce1e27dcc9f4
--- a/src/Pure/ROOT.ML	Wed Oct 02 22:01:04 2019 +0200
+++ b/src/Pure/ROOT.ML	Fri Oct 04 15:30:52 2019 +0200
@@ -150,7 +150,6 @@
 
 ML_file "term_ord.ML";
 ML_file "term_subst.ML";
-ML_file "term_xml.ML";
 ML_file "General/completion.ML";
 ML_file "General/name_space.ML";
 ML_file "sorts.ML";
@@ -161,6 +160,7 @@
 ML_file "item_net.ML";
 ML_file "envir.ML";
 ML_file "consts.ML";
+ML_file "term_xml.ML";
 ML_file "primitive_defs.ML";
 ML_file "sign.ML";
 ML_file "defs.ML";