diff -r b1fd1d756e20 -r 446c5063e4fd src/HOLCF/Sprod.thy --- a/src/HOLCF/Sprod.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOLCF/Sprod.thy Thu Feb 11 23:00:22 2010 +0100 @@ -51,7 +51,7 @@ "ssplit = (\ f. strictify\(\ p. f\(sfst\p)\(ssnd\p)))" syntax - "@stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))") + "_stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))") translations "(:x, y, z:)" == "(:x, (:y, z:):)" "(:x, y:)" == "CONST spair\x\y"