src/ZF/ROOT.ML

--- a/src/ZF/ROOT.ML	Tue Nov 13 22:20:15 2001 +0100
+++ b/src/ZF/ROOT.ML	Tue Nov 13 22:20:51 2001 +0100
@@ -1,35 +1,29 @@
-(*  Title:      ZF/ROOT
+(*  Title:      ZF/ROOT.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Adds Zermelo-Fraenkel Set Theory to a database containing First-Order Logic.
-
-This theory is the work of Martin Coen, Philippe Noel and Lawrence Paulson.
+Zermelo-Fraenkel Set Theory on top of classical First-Order Logic.
+This theory is the work of Martin Coen, Philippe Noel and Lawrence
+Paulson.
 *)
 
 val banner = "ZF Set Theory (in FOL)";
 writeln banner;
 
-eta_contract:=false;
+reset eta_contract;
 
 print_depth 1;
 
-(*Add user sections for inductive/datatype definitions*)
-use     "thy_syntax";
+(*syntax for old-style theory sections*)
+use "thy_syntax";
 
 use "~~/src/Provers/Arith/cancel_numerals.ML";
 use "~~/src/Provers/Arith/combine_numerals.ML";
 
 use_thy "mono";
-use     "ind_syntax.ML";
-use     "Tools/cartprod.ML";
-use_thy "Fixedpt";
-use     "Tools/inductive_package.ML";
-use     "Tools/induct_tacs.ML";
-use     "Tools/primrec_package.ML";
-use_thy "QUniv";
-use     "Tools/datatype_package.ML";
+use "ind_syntax.ML";
+use_thy "Datatype";
 
 use     "Tools/numeral_syntax.ML";
 (*the all-in-one theory*)