src/ZF/QPair.thy
changeset 14854 61bdf2ae4dc5
parent 13823 d49ffd9f9662
child 16417 9bc16273c2d4
--- a/src/ZF/QPair.thy	Tue Jun 01 11:25:26 2004 +0200
+++ b/src/ZF/QPair.thy	Tue Jun 01 12:33:50 2004 +0200
@@ -31,7 +31,7 @@
   qsnd :: "i => i"
     "qsnd(p) == THE b. EX a. p=<a;b>"
 
-  qsplit    :: "[[i, i] => 'a, i] => 'a::logic"  (*for pattern-matching*)
+  qsplit    :: "[[i, i] => 'a, i] => 'a::{}"  (*for pattern-matching*)
     "qsplit(c,p) == c(qfst(p), qsnd(p))"
 
   qconverse :: "i => i"