src/ZF/ROOT.ML

 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;
 
 (*For Pure/tactic??  A crude way of adding structure to rules*)
 fun CHECK_SOLVED tac st =
     case Sequence.pull (tac st) of
         None => error"DO_GOAL: tactic list failed"

 (*Add user sections for inductive/datatype definitions*)
 use     "../Pure/section_utils.ML";
 use     "thy_syntax.ML";
 
 use_thy "Let";
+use_thy "func";
+use     "typechk.ML";
 use_thy "InfDatatype";
 use_thy "List";
 use_thy "EquivClass";
 
 (*printing functions are inherited from FOL*)