src/HOL/IMP/ACom.thy

--- a/src/HOL/IMP/ACom.thy	Wed Sep 05 00:58:54 2012 +0200
+++ b/src/HOL/IMP/ACom.thy	Wed Sep 05 08:32:59 2012 +0200
@@ -16,7 +16,7 @@
   If bexp 'a "('a acom)" 'a "('a acom)" 'a
     ("(IF _/ THEN ({_}/ _)/ ELSE ({_}/ _)//{_})"  [0, 0, 0, 61, 0, 0] 61) |
   While 'a bexp 'a "('a acom)" 'a
-    ("({_}//WHILE _/ DO ({_}/ _)//{_})"  [0, 0, 0, 61, 0] 61)
+    ("({_}//WHILE _//DO ({_}//_)//{_})"  [0, 0, 0, 61, 0] 61)
 
 fun post :: "'a acom \<Rightarrow>'a" where
 "post (SKIP {P}) = P" |