# HG changeset patch
# User wenzelm
# Date 963773599 -7200
# Node ID 82e8b18e698514a209caa286550da265439096f7
# Parent  a4b990838074ff2907c8bd2853636fd776454b7c
more robust tuple syntax (still improper, though!);

diff -r a4b990838074 -r 82e8b18e6985 src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Sun Jul 16 20:52:43 2000 +0200
+++ b/src/HOL/Prod.thy	Sun Jul 16 20:53:19 2000 +0200
@@ -45,21 +45,21 @@
 (* patterns -- extends pre-defined type "pttrn" used in abstractions *)
 
 nonterminals
-  patterns
+  tuple_args patterns
 
 syntax
-  "@Tuple"      :: "['a, args] => 'a * 'b"       ("(1'(_,/ _'))")
-  "_pattern"    :: [pttrn, patterns] => pttrn      ("'(_,/ _')")
-  ""            :: pttrn => patterns                     ("_")
-  "_patterns"   :: [pttrn, patterns] => patterns     ("_,/ _")
-
+  "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1'(_,/ _'))")
+  "_tuple_arg"  :: "'a => tuple_args"                   ("_")
+  "_tuple_args" :: "'a => tuple_args => tuple_args"     ("_,/ _")
+  "_pattern"    :: [pttrn, patterns] => pttrn           ("'(_,/ _')")
+  ""            :: pttrn => patterns                    ("_")
+  "_patterns"   :: [pttrn, patterns] => patterns        ("_,/ _")
   "@Sigma"      :: "[pttrn, 'a set, 'b set] => ('a * 'b) set"   ("(3SIGMA _:_./ _)" 10)
   "@Times"      :: "['a set, 'a => 'b set] => ('a * 'b) set"    (infixr "<*>" 80)
 
 translations
-  "(x, y, z)"    == "(x, (y, z))"
   "(x, y)"       == "Pair x y"
-
+  "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
   "%(x,y,zs).b"  == "split(%x (y,zs).b)"
   "%(x,y).b"     == "split(%x y. b)"
   "_abs (Pair x y) t" => "%(x,y).t"