dedicated exec ... syntax for open state monad (partly already introduces in d00a3f47b607)

--- a/src/HOL/Extraction/Higman.thy	Thu Jul 22 12:07:30 2010 +0200
+++ b/src/HOL/Extraction/Higman.thy	Thu Jul 22 17:26:22 2010 +0200
@@ -350,14 +350,14 @@
 end
 
 function mk_word_aux :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
-  "mk_word_aux k = (do {
+  "mk_word_aux k = exec {
      i \<leftarrow> Random.range 10;
      (if i > 7 \<and> k > 2 \<or> k > 1000 then return []
-     else do {
+     else exec {
        let l = (if i mod 2 = 0 then A else B);
        ls \<leftarrow> mk_word_aux (Suc k);
        return (l # ls)
-     })})"
+     })}"
 by pat_completeness auto
 termination by (relation "measure ((op -) 1001)") auto
 
@@ -366,10 +366,10 @@
 
 primrec mk_word_s :: "nat \<Rightarrow> Random.seed \<Rightarrow> letter list \<times> Random.seed" where
   "mk_word_s 0 = mk_word"
-  | "mk_word_s (Suc n) = (do {
+  | "mk_word_s (Suc n) = exec {
        _ \<leftarrow> mk_word;
        mk_word_s n
-     })"
+     }"
 
 definition g1 :: "nat \<Rightarrow> letter list" where
   "g1 s = fst (mk_word_s s (20000, 1))"