diff -r 61b65ffb4186 -r 9b0142dad559 ex/ROOT.ML
--- a/ex/ROOT.ML	Wed Nov 03 19:02:17 1993 +0100
+++ b/ex/ROOT.ML	Tue Nov 09 11:08:13 1993 +0100
@@ -20,4 +20,5 @@
 time_use_thy "ex/pl";
 time_use_thy "ex/term";
 time_use_thy "ex/simult";
+time_use_thy "ex/mt";
 maketest     "END: Root file for HOL examples";