diff -r 408713c7f66b -r deec279dda0a ex/ROOT.ML
--- a/ex/ROOT.ML	Wed Feb 01 17:18:00 1995 +0100
+++ b/ex/ROOT.ML	Fri Feb 03 16:19:45 1995 +0100
@@ -14,6 +14,7 @@
 time_use     "ex/cla.ML";
 time_use     "ex/meson.ML";
 time_use     "ex/mesontest.ML";
+time_use_thy "String";
 time_use_thy "InSort";
 time_use_thy "Qsort";
 time_use_thy "LexProd";