# HG changeset patch
# User wenzelm
# Date 963773813 -7200
# Node ID 415587dff134b6eeab7272e091d352d1d5ebcf92
# Parent  df7a4824111eec878adf79de38626e0c2fb14d4d
adapted tuple syntax;

diff -r df7a4824111e -r 415587dff134 src/HOL/Modelcheck/MuckeSyn.thy
--- a/src/HOL/Modelcheck/MuckeSyn.thy	Sun Jul 16 20:56:32 2000 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Sun Jul 16 20:56:53 2000 +0200
@@ -39,8 +39,8 @@
 
   "_idts"     	:: [idt, idts] => idts		        ("_,/ _" [1, 0] 0)
 
-  "@Tuple"      :: "['a, args] => 'a * 'b"              ("(1_,/ _)")
-(* "@pttrn"      :: [pttrn, pttrns] => pttrn     	("_,/ _" [1, 0] 0) 
+  "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1_,/ _)")
+(* "@pttrn"     :: [pttrn, pttrns] => pttrn     	("_,/ _" [1, 0] 0) 
   "_pattern"    :: [pttrn, patterns] => pttrn           ("_,/ _" [1, 0] 0) *)