# HG changeset patch
# User haftmann
# Date 1207755977 -7200
# Node ID 43cb72871897c07b46824335488f7c2bf9694692
# Parent  d83271bfaba5437fcb98d29c92b6507682f15b4b
renamed mbind to scomp

diff -r d83271bfaba5 -r 43cb72871897 src/HOL/ex/Quickcheck.thy
--- a/src/HOL/ex/Quickcheck.thy	Wed Apr 09 08:10:11 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy	Wed Apr 09 17:46:17 2008 +0200
@@ -42,8 +42,8 @@
   fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
   fun mk_split thy ty ty' = Sign.mk_const thy
     (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT (term_ty ty') @{typ seed}]);
-  fun mk_mbind_split thy ty ty' t t' =
-    StateMonad.mbind (term_ty ty) (term_ty ty') @{typ seed} t
+  fun mk_scomp_split thy ty ty' t t' =
+    StateMonad.scomp (term_ty ty) (term_ty ty') @{typ seed} t
       (mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')))
   fun mk_cons thy this_ty (c, args) =
     let
@@ -59,7 +59,7 @@
       val return = StateMonad.return (term_ty this_ty) @{typ seed}
         (HOLogic.mk_prod (c_t, t_t));
       val t = fold_rev (fn ((ty, _), random) =>
-        mk_mbind_split thy ty this_ty random)
+        mk_scomp_split thy ty this_ty random)
           args return;
       val is_rec = exists (snd o fst) args;
     in (is_rec, StateMonad.run (term_ty this_ty) @{typ seed} t) end;
@@ -268,10 +268,10 @@
     fun mk_termtyp ty = HOLogic.mk_prodT (ty, @{typ "unit \<Rightarrow> term"});
     fun mk_split ty = Sign.mk_const thy
       (@{const_name split}, [ty, @{typ "unit \<Rightarrow> term"}, StateMonad.liftT @{typ "term list option"} @{typ seed}]);
-    fun mk_mbind_split ty t t' =
-      StateMonad.mbind (mk_termtyp ty) @{typ "term list option"} @{typ seed} t (*FIXME*)
+    fun mk_scomp_split ty t t' =
+      StateMonad.scomp (mk_termtyp ty) @{typ "term list option"} @{typ seed} t (*FIXME*)
         (mk_split ty $ Abs ("", ty, Abs ("", @{typ "unit \<Rightarrow> term"}, t')));
-    fun mk_bindclause (_, _, i, ty) = mk_mbind_split ty
+    fun mk_bindclause (_, _, i, ty) = mk_scomp_split ty
       (Sign.mk_const thy (@{const_name random}, [ty]) $ Bound i)
     val t = fold_rev mk_bindclause bounds (return $ check);
   in Abs ("n", @{typ index}, t) end;
diff -r d83271bfaba5 -r 43cb72871897 src/HOL/ex/Random.thy
--- a/src/HOL/ex/Random.thy	Wed Apr 09 08:10:11 2008 +0200
+++ b/src/HOL/ex/Random.thy	Wed Apr 09 17:46:17 2008 +0200
@@ -114,7 +114,7 @@
     "range_aux (log 2147483561 k) 1 s = (v, w)"
     by (cases "range_aux (log 2147483561 k) 1 s")
   with assms show ?thesis
-    by (simp add: range_def run_def mbind_def split_def del: range_aux.simps log.simps)
+    by (simp add: range_def run_def scomp_def split_def del: range_aux.simps log.simps)
 qed
 
 definition
@@ -135,7 +135,7 @@
   then have
     "nat_of_index (fst (range (index_of_nat (length xs)) s)) < length xs" by simp
   then show ?thesis
-    by (auto simp add: select_def run_def mbind_def split_def)
+    by (auto simp add: select_def run_def scomp_def split_def)
 qed
 
 definition
@@ -148,7 +148,7 @@
 
 lemma select_default_zero:
   "fst (select_default 0 x y s) = y"
-  by (simp add: run_def mbind_def split_def select_default_def)
+  by (simp add: run_def scomp_def split_def select_default_def)
 
 lemma select_default_code [code]:
   "select_default k x y = (if k = 0 then do
@@ -162,7 +162,7 @@
   case False then show ?thesis by (simp add: select_default_def)
 next
   case True then show ?thesis
-    by (simp add: run_def mbind_def split_def select_default_def expand_fun_eq range_def)
+    by (simp add: run_def scomp_def split_def select_default_def expand_fun_eq range_def)
 qed