src/ZF/QPair.thy

--- a/src/ZF/QPair.thy	Fri Oct 08 14:11:12 1993 +0100
+++ b/src/ZF/QPair.thy	Fri Oct 08 14:16:29 1993 +0100
@@ -27,6 +27,7 @@
 
 translations
   "QSUM x:A. B"  => "QSigma(A, %x. B)"
+  "A <*> B"      => "QSigma(A, _K(B))"
 
 rules
   QPair_def       "<a;b> == a+b"
@@ -43,10 +44,5 @@
 
 ML
 
-(* 'Dependent' type operators *)
-
-val parse_translation =
-  [(" <*>", ndependent_tr "QSigma")];
-
 val print_translation =
   [("QSigma", dependent_tr' ("@QSUM", " <*>"))];