diff -r 428efffe8599 -r b50b8c0eec01 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Fri Jan 03 10:48:28 1997 +0100
+++ b/src/ZF/ROOT.ML	Fri Jan 03 15:01:55 1997 +0100
@@ -11,6 +11,8 @@
 val banner = "ZF Set Theory (in FOL)";
 writeln banner;
 
+eta_contract:=false;
+
 (*For Pure/tactic??  A crude way of adding structure to rules*)
 fun CHECK_SOLVED tac st =
     case Sequence.pull (tac st) of
@@ -32,6 +34,8 @@
 use     "thy_syntax.ML";
 
 use_thy "Let";
+use_thy "func";
+use     "typechk.ML";
 use_thy "InfDatatype";
 use_thy "List";
 use_thy "EquivClass";