src/ZF/QPair.thy

--- a/src/ZF/QPair.thy	Tue Jan 12 13:54:51 1999 +0100
+++ b/src/ZF/QPair.thy	Tue Jan 12 15:17:37 1999 +0100
@@ -13,8 +13,6 @@
 
 QPair = Sum +
 
-global
-
 consts
   QPair     :: [i, i] => i                      ("<(_;/ _)>")
   qfst,qsnd :: i => i
@@ -34,7 +32,6 @@
   "QSUM x:A. B"  => "QSigma(A, %x. B)"
   "A <*> B"      => "QSigma(A, _K(B))"
 
-local
 
 defs
   QPair_def       "<a;b> == a+b"