diff -r e384e27c229f -r 0015a0a99ae9 src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Thu Feb 11 21:31:50 2010 +0100
+++ b/src/HOL/Metis_Examples/Message.thy	Thu Feb 11 21:33:25 2010 +0100
@@ -45,10 +45,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|}|}"