diff -r 5b96b1252cdc -r 93dc86ccee28 ROOT.ML
--- a/ROOT.ML	Fri Aug 19 11:19:14 1994 +0200
+++ b/ROOT.ML	Fri Aug 19 11:25:16 1994 +0200
@@ -77,13 +77,10 @@
 
 use     "simpdata.ML";
 use_thy "Ord";
-use_thy "Set";
-use     "fun.ML";
-use     "subset.ML";
-use     "equalities.ML";
+use_thy "subset";
+use_thy "equalities";
 use_thy "Prod";
 use_thy "Sum";
-use     "mono.ML";
 use_thy "LList";
 
 use "../Pure/install_pp.ML";