--- a/src/ZF/ZF.thy Fri Sep 03 22:57:21 2010 +0200
+++ b/src/ZF/ZF.thy Fri Sep 03 23:54:48 2010 +0200
@@ -10,7 +10,7 @@
uses "~~/src/Tools/misc_legacy.ML"
begin
-ML {* eta_contract := false *}
+declare [[eta_contract = false]]
typedecl i
arities i :: "term"