# HG changeset patch
# User paulson
# Date 841770443 -7200
# Node ID f19a801a2bcaea1f93c7877ed90f0824d306365c
# Parent  b59a3d686436fb0afd56a1136eb3bc7d058a7fec
Fixed pretty-printing of {|...|}

diff -r b59a3d686436 -r f19a801a2bca 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|}|}"