src/ZF/ROOT.ML

--- a/src/ZF/ROOT.ML	Fri Jun 30 12:49:11 2000 +0200
+++ b/src/ZF/ROOT.ML	Fri Jun 30 12:51:30 2000 +0200
@@ -18,7 +18,6 @@
 (*Add user sections for inductive/datatype definitions*)
 use     "thy_syntax";
 
-use_thy "Let";
 use_thy "ZF";
 use     "Tools/typechk";
 use_thy "mono";
@@ -28,7 +27,6 @@
 use     "Tools/inductive_package";
 use     "Tools/induct_tacs";
 use     "Tools/primrec_package";
-use_thy "Inductive";
 use_thy "QUniv";
 use     "Tools/datatype_package";