--- a/src/ZF/ZF.thy Mon Feb 10 14:33:47 2014 +0100
+++ b/src/ZF/ZF.thy Mon Feb 10 17:20:11 2014 +0100
@@ -12,7 +12,7 @@
declare [[eta_contract = false]]
typedecl i
-arities i :: "term"
+instance i :: "term" ..
axiomatization
zero :: "i" ("0") --{*the empty set*} and