--- a/src/ZF/ZF.thy Fri Aug 27 12:57:55 2010 +0200
+++ b/src/ZF/ZF.thy Fri Aug 27 14:07:09 2010 +0200
@@ -10,7 +10,7 @@
uses "~~/src/Tools/misc_legacy.ML"
begin
-ML {* Unsynchronized.reset eta_contract *}
+ML {* eta_contract := false *}
typedecl i
arities i :: "term"