--- a/src/Pure/ROOT.ML Tue Oct 26 15:11:40 2021 +0200
+++ b/src/Pure/ROOT.ML Tue Oct 26 16:01:05 2021 +0200
@@ -339,6 +339,7 @@
ML_file "ML/ml_pp.ML";
ML_file "ML/ml_thms.ML";
+ML_file "ML/ml_instantiate.ML";
ML_file "ML/ml_file.ML";
ML_file "Tools/build.ML";