src/HOL/Auth/Message.thy

--- a/src/HOL/Auth/Message.thy	Tue Sep 03 19:07:00 1996 +0200
+++ b/src/HOL/Auth/Message.thy	Tue Sep 03 19:07:23 1996 +0200
@@ -55,7 +55,7 @@
 
 (*Allows messages of the form {|A,B,NA|}, etc...*)
 syntax
-  "@MTuple"      :: "['a, args] => 'a * 'b"            ("(1{|_,/ _|})")
+  "@MTuple"      :: "['a, args] => 'a * 'b"            ("(2{|_,/ _|})")
 
 translations
   "{|x, y, z|}"   == "{|x, {|y, z|}|}"