src/ZF/ZF.thy

--- a/src/ZF/ZF.thy	Tue Jun 01 11:25:26 2004 +0200
+++ b/src/ZF/ZF.thy	Tue Jun 01 12:33:50 2004 +0200
@@ -61,7 +61,7 @@
   Pair  :: "[i, i] => i"
   fst   :: "i => i"
   snd   :: "i => i"
-  split :: "[[i, i] => 'a, i] => 'a::logic"  --{*for pattern-matching*}
+  split :: "[[i, i] => 'a, i] => 'a::{}"  --{*for pattern-matching*}
 
 text {*Sigma and Pi Operators *}
 consts