--- a/src/ZF/ZF.thy Mon Jul 12 21:12:18 2010 +0200
+++ b/src/ZF/ZF.thy Mon Jul 12 21:38:37 2010 +0200
@@ -5,7 +5,10 @@
header{*Zermelo-Fraenkel Set Theory*}
-theory ZF imports FOL begin
+theory ZF
+imports FOL
+uses "~~/src/Tools/misc_legacy.ML"
+begin
ML {* Unsynchronized.reset eta_contract *}