diff -r 32a83e3ad5a4 -r 94436622324d ex/ROOT.ML
--- a/ex/ROOT.ML	Sun Mar 27 12:36:39 1994 +0200
+++ b/ex/ROOT.ML	Sun Mar 27 16:43:06 1994 +0200
@@ -18,6 +18,7 @@
 time_use_thy "Qsort";
 time_use_thy "LexProd";
 time_use_thy "Puzzle";
+time_use_thy "NatSum";
 time_use     "ex/set.ML";
 time_use_thy "PL";
 time_use_thy "Term";