# HG changeset patch
# User nipkow
# Date 1323066671 -3600
# Node ID b5db02fa9536b1cf2650a6a865f8a32b03c0be3a
# Parent  17100f4ce0b5d7977d4570337592f7bd0610723a# Parent  f8723843c29e6357db3214da172805ad24d0958f
merged

diff -r 17100f4ce0b5 -r b5db02fa9536 src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Sun Dec 04 20:05:08 2011 +0100
+++ b/src/HOL/IMP/ACom.thy	Mon Dec 05 07:31:11 2011 +0100
@@ -10,7 +10,7 @@
 section "Annotated Commands"
 
 datatype 'a acom =
-  SKIP   'a                           ("SKIP {_}") |
+  SKIP   'a                           ("SKIP {_}" 61) |
   Assign vname aexp 'a                ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
   Semi   "('a acom)" "('a acom)"          ("_;//_"  [60, 61] 60) |
   If     bexp "('a acom)" "('a acom)" 'a