diff -r e103e3cef3cb -r 8fb4013f2ac2 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Dec 01 10:10:59 2023 +0100
+++ b/src/Pure/ROOT.ML	Fri Dec 01 16:10:09 2023 +0100
@@ -168,15 +168,15 @@
 ML_file "item_net.ML";
 ML_file "envir.ML";
 ML_file "consts.ML";
-ML_file "zterm.ML";
-ML_file "term_xml.ML";
 ML_file "primitive_defs.ML";
 ML_file "sign.ML";
 ML_file "defs.ML";
-ML_file "term_sharing.ML";
 ML_file "pattern.ML";
 ML_file "unify.ML";
 ML_file "theory.ML";
+ML_file "term_sharing.ML";
+ML_file "term_xml.ML";
+ML_file "zterm.ML";
 ML_file "proofterm.ML";
 ML_file "thm.ML";
 ML_file "cterm_items.ML";