src/ZF/Constructible/MetaExists.thy

--- a/src/ZF/Constructible/MetaExists.thy	Tue Jun 01 11:25:26 2004 +0200
+++ b/src/ZF/Constructible/MetaExists.thy	Tue Jun 01 12:33:50 2004 +0200
@@ -11,7 +11,7 @@
 quantify over classes.  Yields a proposition rather than a FOL formula.*}
 
 constdefs
-  ex :: "(('a::logic) => prop) => prop"            (binder "?? " 0)
+  ex :: "(('a::{}) => prop) => prop"            (binder "?? " 0)
   "ex(P) == (!!Q. (!!x. PROP P(x) ==> PROP Q) ==> PROP Q)"
 
 syntax (xsymbols)