diff -r 9174de6c7143 -r d63ffafce255 src/HOLCF/Sprod3.thy
--- a/src/HOLCF/Sprod3.thy	Fri Nov 29 12:17:30 1996 +0100
+++ b/src/HOLCF/Sprod3.thy	Fri Nov 29 12:22:22 1996 +0100
@@ -34,6 +34,12 @@
 ssplit_def      "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))"
 
 (* start 8bit 1 *)
+syntax  
+	"@Gstuple"    :: "['a, args] => 'a ** 'b"	("(1É_,/ _Ê)")
+
+translations
+	"Éx, y, zÊ"   == "Éx, Éy, zÊÊ"
+	"Éx, yÊ"      == "(|x,y|)"
 (* end 8bit 1 *)
 
 end