# HG changeset patch
# User wenzelm
# Date 1180628219 -7200
# Node ID fcdd4346fa6bc3424c7ea99556a827f7243bc3e5
# Parent  b9bbdf7eab3b203deb0ec32d621c3af3688cc7f1
tuned ML setup;

diff -r b9bbdf7eab3b -r fcdd4346fa6b src/ZF/ROOT.ML
--- 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*)
diff -r b9bbdf7eab3b -r fcdd4346fa6b src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Thu May 31 18:16:58 2007 +0200
+++ b/src/ZF/ZF.thy	Thu May 31 18:16:59 2007 +0200
@@ -8,6 +8,8 @@
 
 theory ZF imports FOL begin
 
+ML {* reset eta_contract *}
+
 global
 
 typedecl i