# HG changeset patch
# User nipkow
# Date 1323066660 -3600
# Node ID f8723843c29e6357db3214da172805ad24d0958f
# Parent  8b05cda62000639c384b36e58a3c006a8ead91d0
enforce parantheses around SKIP {_}

diff -r 8b05cda62000 -r f8723843c29e src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Sun Dec 04 18:29:29 2011 +0100
+++ b/src/HOL/IMP/ACom.thy	Mon Dec 05 07:31:00 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