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";