--- a/src/HOL/Auth/Message.thy Thu Feb 11 21:31:50 2010 +0100
+++ b/src/HOL/Auth/Message.thy Thu Feb 11 21:33:25 2010 +0100
@@ -51,10 +51,10 @@
text{*Concrete syntax: messages appear as {|A,B,NA|}, etc...*}
syntax
- "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
+ "_MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})")
syntax (xsymbols)
- "@MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
+ "_MTuple" :: "['a, args] => 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)")
translations
"{|x, y, z|}" == "{|x, {|y, z|}|}"