diff -r 715d01b34abb -r a7daa74e2980 src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Thu Apr 26 13:33:17 2007 +0200
+++ b/src/ZF/QPair.thy	Thu Apr 26 14:24:08 2007 +0200
@@ -41,12 +41,13 @@
     "QSigma(A,B)  ==  \<Union>x\<in>A. \<Union>y\<in>B(x). {<x;y>}"
 
 syntax
-  "@QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
-  "<*>"     :: "[i, i] => i"                      (infixr 80)
-
+  "_QSUM"   :: "[idt, i, i] => i"               ("(3QSUM _:_./ _)" 10)
 translations
   "QSUM x:A. B"  => "QSigma(A, %x. B)"
-  "A <*> B"      => "QSigma(A, %_. B)"
+
+abbreviation
+  qprod  (infixr "<*>" 80) where
+  "A <*> B == QSigma(A, %_. B)"
 
 constdefs
   qsum    :: "[i,i]=>i"                         (infixr "<+>" 65)
@@ -62,9 +63,6 @@
     "qcase(c,d)   == qsplit(%y z. cond(y, d(z), c(z)))"
 
 
-print_translation {* [("QSigma", dependent_tr' ("@QSUM", "op <*>"))] *}
-
-
 subsection{*Quine ordered pairing*}
 
 (** Lemmas for showing that <a;b> uniquely determines a and b **)
@@ -386,4 +384,3 @@
 *}
 
 end
-