# HG changeset patch
# User haftmann
# Date 1279812391 -7200
# Node ID 7551769de556d4e0a9a74cfccd510da7262ccd72
# Parent  b8ca89c45086a8ff76c6d7d1bcf3a96a71da96eb# Parent  440114da2488a8110d8f03ac9ef213d3e1e1ab7e
merged

diff -r b8ca89c45086 -r 7551769de556 src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Thu Jul 22 16:53:00 2010 +0200
+++ b/src/HOL/Extraction/Higman.thy	Thu Jul 22 17:26:31 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))"