--- a/src/Pure/ROOT.ML Fri Apr 14 20:42:17 2023 +0200
+++ b/src/Pure/ROOT.ML Fri Apr 14 21:34:51 2023 +0200
@@ -19,6 +19,7 @@
ML_file "ML/ml_system.ML";
ML_file "General/basics.ML";
+ML_file "General/string.ML";
ML_file "General/vector.ML";
ML_file "General/symbol_explode.ML";