diff -r b93cc55cb7ab -r df6b3bd14dcb ex/ROOT.ML --- a/ex/ROOT.ML Fri Dec 02 11:43:20 1994 +0100 +++ b/ex/ROOT.ML Fri Dec 02 16:09:49 1994 +0100 @@ -20,6 +20,7 @@ time_use_thy "Puzzle"; time_use_thy "NatSum"; time_use "ex/set.ML"; +time_use_thy "SList"; time_use_thy "LList"; time_use_thy "Acc"; time_use_thy "PropLog";