--- a/src/ZF/ROOT.ML Thu May 31 18:16:58 2007 +0200
+++ b/src/ZF/ROOT.ML Thu May 31 18:16:59 2007 +0200
@@ -11,8 +11,6 @@
val banner = "ZF Set Theory (in FOL)";
writeln banner;
-reset eta_contract;
-
use_thy "Main_ZFC";
Goal "True"; (*leave subgoal package empty*)