diff -r 0d6b64060543 -r ba0bc31b90d7 src/HOL/Imperative_HOL/Mrec.thy
--- a/src/HOL/Imperative_HOL/Mrec.thy	Tue Jul 13 11:50:22 2010 +0200
+++ b/src/HOL/Imperative_HOL/Mrec.thy	Tue Jul 13 12:00:11 2010 +0200
@@ -64,13 +64,12 @@
 
 lemma MREC_rule:
   "MREC x = 
-  (do y \<leftarrow> f x;
+  do { y \<leftarrow> f x;
                 (case y of 
                 Inl r \<Rightarrow> return r
               | Inr s \<Rightarrow> 
-                do z \<leftarrow> MREC s ;
-                   g x s z
-                done) done)"
+                do { z \<leftarrow> MREC s ;
+                     g x s z })}"
   unfolding MREC_def
   unfolding bind_def return_def
   apply simp