using more conventional names for monad plus operations
authorbulwahn
Fri Nov 11 12:10:49 2011 +0100 (2011-11-11)
changeset 45461130c90bb80b4
parent 45452 414732ebf891
child 45465 77c5b334a7ae
using more conventional names for monad plus operations
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
     1.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Nov 11 10:40:36 2011 +0100
     1.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Fri Nov 11 12:10:49 2011 +0100
     1.3 @@ -100,12 +100,12 @@
     1.4    val minus_nat = Core_Data.functional_compilation @{const_name "minus"} iio
     1.5    fun subtract_nat compfuns (_ : typ) =
     1.6      let
     1.7 -      val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
     1.8 +      val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
     1.9      in
    1.10        absdummy @{typ nat} (absdummy @{typ nat}
    1.11          (Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
    1.12            (@{term "op > :: nat => nat => bool"} $ Bound 1 $ Bound 0) $
    1.13 -          Predicate_Compile_Aux.mk_bot compfuns @{typ nat} $
    1.14 +          Predicate_Compile_Aux.mk_empty compfuns @{typ nat} $
    1.15            Predicate_Compile_Aux.mk_single compfuns
    1.16            (@{term "op - :: nat => nat => nat"} $ Bound 0 $ Bound 1)))
    1.17      end
    1.18 @@ -118,7 +118,7 @@
    1.19    fun enumerate_nats compfuns  (_ : typ) =
    1.20      let
    1.21        val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"})
    1.22 -      val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
    1.23 +      val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
    1.24      in
    1.25        absdummy @{typ nat} (absdummy @{typ nat}
    1.26          (Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Nov 11 10:40:36 2011 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Nov 11 12:10:49 2011 +0100
     2.3 @@ -66,23 +66,23 @@
     2.4    val find_split_thm : theory -> term -> thm option
     2.5    (* datastructures and setup for generic compilation *)
     2.6    datatype compilation_funs = CompilationFuns of {
     2.7 -    mk_predT : typ -> typ,
     2.8 -    dest_predT : typ -> typ,
     2.9 -    mk_bot : typ -> term,
    2.10 +    mk_monadT : typ -> typ,
    2.11 +    dest_monadT : typ -> typ,
    2.12 +    mk_empty : typ -> term,
    2.13      mk_single : term -> term,
    2.14      mk_bind : term * term -> term,
    2.15 -    mk_sup : term * term -> term,
    2.16 +    mk_plus : term * term -> term,
    2.17      mk_if : term -> term,
    2.18      mk_iterate_upto : typ -> term * term * term -> term,
    2.19      mk_not : term -> term,
    2.20      mk_map : typ -> typ -> term -> term -> term
    2.21    };
    2.22 -  val mk_predT : compilation_funs -> typ -> typ
    2.23 -  val dest_predT : compilation_funs -> typ -> typ
    2.24 -  val mk_bot : compilation_funs -> typ -> term
    2.25 +  val mk_monadT : compilation_funs -> typ -> typ
    2.26 +  val dest_monadT : compilation_funs -> typ -> typ
    2.27 +  val mk_empty : compilation_funs -> typ -> term
    2.28    val mk_single : compilation_funs -> term -> term
    2.29    val mk_bind : compilation_funs -> term * term -> term
    2.30 -  val mk_sup : compilation_funs -> term * term -> term
    2.31 +  val mk_plus : compilation_funs -> term * term -> term
    2.32    val mk_if : compilation_funs -> term -> term
    2.33    val mk_iterate_upto : compilation_funs -> typ -> term * term * term -> term
    2.34    val mk_not : compilation_funs -> term -> term
    2.35 @@ -699,24 +699,24 @@
    2.36  (* datastructures and setup for generic compilation *)
    2.37  
    2.38  datatype compilation_funs = CompilationFuns of {
    2.39 -  mk_predT : typ -> typ,
    2.40 -  dest_predT : typ -> typ,
    2.41 -  mk_bot : typ -> term,
    2.42 +  mk_monadT : typ -> typ,
    2.43 +  dest_monadT : typ -> typ,
    2.44 +  mk_empty : typ -> term,
    2.45    mk_single : term -> term,
    2.46    mk_bind : term * term -> term,
    2.47 -  mk_sup : term * term -> term,
    2.48 +  mk_plus : term * term -> term,
    2.49    mk_if : term -> term,
    2.50    mk_iterate_upto : typ -> term * term * term -> term,
    2.51    mk_not : term -> term,
    2.52    mk_map : typ -> typ -> term -> term -> term
    2.53  };
    2.54  
    2.55 -fun mk_predT (CompilationFuns funs) = #mk_predT funs
    2.56 -fun dest_predT (CompilationFuns funs) = #dest_predT funs
    2.57 -fun mk_bot (CompilationFuns funs) = #mk_bot funs
    2.58 +fun mk_monadT (CompilationFuns funs) = #mk_monadT funs
    2.59 +fun dest_monadT (CompilationFuns funs) = #dest_monadT funs
    2.60 +fun mk_empty (CompilationFuns funs) = #mk_empty funs
    2.61  fun mk_single (CompilationFuns funs) = #mk_single funs
    2.62  fun mk_bind (CompilationFuns funs) = #mk_bind funs
    2.63 -fun mk_sup (CompilationFuns funs) = #mk_sup funs
    2.64 +fun mk_plus (CompilationFuns funs) = #mk_plus funs
    2.65  fun mk_if (CompilationFuns funs) = #mk_if funs
    2.66  fun mk_iterate_upto (CompilationFuns funs) = #mk_iterate_upto funs
    2.67  fun mk_not (CompilationFuns funs) = #mk_not funs
    2.68 @@ -729,7 +729,7 @@
    2.69      val Ts = binder_types T
    2.70      val (inTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode Ts
    2.71    in
    2.72 -    inTs ---> (mk_predT compfuns (HOLogic.mk_tupleT outTs))
    2.73 +    inTs ---> (mk_monadT compfuns (HOLogic.mk_tupleT outTs))
    2.74    end;
    2.75  
    2.76  (* Different options for compiler *)
     3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Fri Nov 11 10:40:36 2011 +0100
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_compilations.ML	Fri Nov 11 12:10:49 2011 +0100
     3.3 @@ -7,16 +7,16 @@
     3.4  structure Predicate_Comp_Funs =
     3.5  struct
     3.6  
     3.7 -fun mk_predT T = Type (@{type_name Predicate.pred}, [T])
     3.8 +fun mk_monadT T = Type (@{type_name Predicate.pred}, [T])
     3.9  
    3.10 -fun dest_predT (Type (@{type_name Predicate.pred}, [T])) = T
    3.11 -  | dest_predT T = raise TYPE ("dest_predT", [T], []);
    3.12 +fun dest_monadT (Type (@{type_name Predicate.pred}, [T])) = T
    3.13 +  | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
    3.14  
    3.15 -fun mk_bot T = Const (@{const_name Orderings.bot}, mk_predT T);
    3.16 +fun mk_empty T = Const (@{const_name Orderings.bot}, mk_monadT T);
    3.17  
    3.18  fun mk_single t =
    3.19    let val T = fastype_of t
    3.20 -  in Const(@{const_name Predicate.single}, T --> mk_predT T) $ t end;
    3.21 +  in Const(@{const_name Predicate.single}, T --> mk_monadT T) $ t end;
    3.22  
    3.23  fun mk_bind (x, f) =
    3.24    let val T as Type ("fun", [_, U]) = fastype_of f
    3.25 @@ -24,42 +24,42 @@
    3.26      Const (@{const_name Predicate.bind}, fastype_of x --> T --> U) $ x $ f
    3.27    end;
    3.28  
    3.29 -val mk_sup = HOLogic.mk_binop @{const_name sup};
    3.30 +val mk_plus = HOLogic.mk_binop @{const_name sup};
    3.31  
    3.32  fun mk_if cond = Const (@{const_name Predicate.if_pred},
    3.33 -  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
    3.34 +  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
    3.35  
    3.36  fun mk_iterate_upto T (f, from, to) =
    3.37    list_comb (Const (@{const_name Code_Numeral.iterate_upto},
    3.38 -      [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_predT T),
    3.39 +      [@{typ code_numeral} --> T, @{typ code_numeral}, @{typ code_numeral}] ---> mk_monadT T),
    3.40      [f, from, to])
    3.41  
    3.42  fun mk_not t =
    3.43    let
    3.44 -    val T = mk_predT HOLogic.unitT
    3.45 +    val T = mk_monadT HOLogic.unitT
    3.46    in Const (@{const_name Predicate.not_pred}, T --> T) $ t end
    3.47  
    3.48  fun mk_Enum f =
    3.49    let val T as Type ("fun", [T', _]) = fastype_of f
    3.50    in
    3.51 -    Const (@{const_name Predicate.Pred}, T --> mk_predT T') $ f    
    3.52 +    Const (@{const_name Predicate.Pred}, T --> mk_monadT T') $ f    
    3.53    end;
    3.54  
    3.55  fun mk_Eval (f, x) =
    3.56    let
    3.57 -    val T = dest_predT (fastype_of f)
    3.58 +    val T = dest_monadT (fastype_of f)
    3.59    in
    3.60 -    Const (@{const_name Predicate.eval}, mk_predT T --> T --> HOLogic.boolT) $ f $ x
    3.61 +    Const (@{const_name Predicate.eval}, mk_monadT T --> T --> HOLogic.boolT) $ f $ x
    3.62    end;
    3.63  
    3.64  fun dest_Eval (Const (@{const_name Predicate.eval}, _) $ f $ x) = (f, x)
    3.65  
    3.66  fun mk_map T1 T2 tf tp = Const (@{const_name Predicate.map},
    3.67 -  (T1 --> T2) --> mk_predT T1 --> mk_predT T2) $ tf $ tp;
    3.68 +  (T1 --> T2) --> mk_monadT T1 --> mk_monadT T2) $ tf $ tp;
    3.69  
    3.70  val compfuns = Predicate_Compile_Aux.CompilationFuns
    3.71 -    {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
    3.72 -    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
    3.73 +    {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
    3.74 +    mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
    3.75      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
    3.76  
    3.77  end;
    3.78 @@ -67,16 +67,16 @@
    3.79  structure CPS_Comp_Funs =
    3.80  struct
    3.81  
    3.82 -fun mk_predT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"}
    3.83 +fun mk_monadT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "Code_Evaluation.term list option"}
    3.84  
    3.85 -fun dest_predT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = T
    3.86 -  | dest_predT T = raise TYPE ("dest_predT", [T], []);
    3.87 +fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "term list option"}])) = T
    3.88 +  | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
    3.89  
    3.90 -fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_predT T);
    3.91 +fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.cps_empty}, mk_monadT T);
    3.92  
    3.93  fun mk_single t =
    3.94    let val T = fastype_of t
    3.95 -  in Const(@{const_name Quickcheck_Exhaustive.cps_single}, T --> mk_predT T) $ t end;
    3.96 +  in Const(@{const_name Quickcheck_Exhaustive.cps_single}, T --> mk_monadT T) $ t end;
    3.97  
    3.98  fun mk_bind (x, f) =
    3.99    let val T as Type ("fun", [_, U]) = fastype_of f
   3.100 @@ -84,16 +84,16 @@
   3.101      Const (@{const_name Quickcheck_Exhaustive.cps_bind}, fastype_of x --> T --> U) $ x $ f
   3.102    end;
   3.103  
   3.104 -val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus};
   3.105 +val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.cps_plus};
   3.106  
   3.107  fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.cps_if},
   3.108 -  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
   3.109 +  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
   3.110  
   3.111  fun mk_iterate_upto T (f, from, to) = error "not implemented yet"
   3.112  
   3.113  fun mk_not t =
   3.114    let
   3.115 -    val T = mk_predT HOLogic.unitT
   3.116 +    val T = mk_monadT HOLogic.unitT
   3.117    in Const (@{const_name Quickcheck_Exhaustive.cps_not}, T --> T) $ t end
   3.118  
   3.119  fun mk_Enum f = error "not implemented"
   3.120 @@ -105,8 +105,8 @@
   3.121  fun mk_map T1 T2 tf tp = error "not implemented"
   3.122  
   3.123  val compfuns = Predicate_Compile_Aux.CompilationFuns
   3.124 -    {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
   3.125 -    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.126 +    {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
   3.127 +    mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
   3.128      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
   3.129  
   3.130  end;
   3.131 @@ -114,16 +114,16 @@
   3.132  structure Pos_Bounded_CPS_Comp_Funs =
   3.133  struct
   3.134  
   3.135 -fun mk_predT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "code_numeral => Code_Evaluation.term list option"}
   3.136 +fun mk_monadT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ "code_numeral => Code_Evaluation.term list option"}
   3.137  
   3.138 -fun dest_predT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "code_numeral => term list option"}])) = T
   3.139 -  | dest_predT T = raise TYPE ("dest_predT", [T], []);
   3.140 +fun dest_monadT (Type ("fun", [Type ("fun", [T, @{typ "term list option"}]), @{typ "code_numeral => term list option"}])) = T
   3.141 +  | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
   3.142  
   3.143 -fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_predT T);
   3.144 +fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_empty}, mk_monadT T);
   3.145  
   3.146  fun mk_single t =
   3.147    let val T = fastype_of t
   3.148 -  in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, T --> mk_predT T) $ t end;
   3.149 +  in Const(@{const_name Quickcheck_Exhaustive.pos_bound_cps_single}, T --> mk_monadT T) $ t end;
   3.150  
   3.151  fun mk_bind (x, f) =
   3.152    let val T as Type ("fun", [_, U]) = fastype_of f
   3.153 @@ -131,10 +131,10 @@
   3.154      Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
   3.155    end;
   3.156  
   3.157 -val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus};
   3.158 +val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.pos_bound_cps_plus};
   3.159  
   3.160  fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_if},
   3.161 -  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
   3.162 +  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
   3.163  
   3.164  fun mk_iterate_upto T (f, from, to) = error "not implemented yet"
   3.165  
   3.166 @@ -143,7 +143,7 @@
   3.167      val nT = @{typ "(unit Quickcheck_Exhaustive.unknown =>
   3.168        Code_Evaluation.term list Quickcheck_Exhaustive.three_valued) => code_numeral =>
   3.169        Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}
   3.170 -    val T = mk_predT HOLogic.unitT
   3.171 +    val T = mk_monadT HOLogic.unitT
   3.172    in Const (@{const_name Quickcheck_Exhaustive.pos_bound_cps_not}, nT --> T) $ t end
   3.173  
   3.174  fun mk_Enum f = error "not implemented"
   3.175 @@ -155,8 +155,8 @@
   3.176  fun mk_map T1 T2 tf tp = error "not implemented"
   3.177  
   3.178  val compfuns = Predicate_Compile_Aux.CompilationFuns
   3.179 -    {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
   3.180 -    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.181 +    {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
   3.182 +    mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
   3.183      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
   3.184  
   3.185  end;
   3.186 @@ -164,21 +164,21 @@
   3.187  structure Neg_Bounded_CPS_Comp_Funs =
   3.188  struct
   3.189  
   3.190 -fun mk_predT T =
   3.191 +fun mk_monadT T =
   3.192    (Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T])
   3.193      --> @{typ "Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"})
   3.194      --> @{typ "code_numeral => Code_Evaluation.term list Quickcheck_Exhaustive.three_valued"}
   3.195  
   3.196 -fun dest_predT (Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]),
   3.197 +fun dest_monadT (Type ("fun", [Type ("fun", [Type (@{type_name "Quickcheck_Exhaustive.unknown"}, [T]),
   3.198      @{typ "term list Quickcheck_Exhaustive.three_valued"}]),
   3.199      @{typ "code_numeral => term list Quickcheck_Exhaustive.three_valued"}])) = T
   3.200 -  | dest_predT T = raise TYPE ("dest_predT", [T], []);
   3.201 +  | dest_monadT T = raise TYPE ("dest_monadT", [T], []);
   3.202  
   3.203 -fun mk_bot T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_predT T);
   3.204 +fun mk_empty T = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_empty}, mk_monadT T);
   3.205  
   3.206  fun mk_single t =
   3.207    let val T = fastype_of t
   3.208 -  in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, T --> mk_predT T) $ t end;
   3.209 +  in Const(@{const_name Quickcheck_Exhaustive.neg_bound_cps_single}, T --> mk_monadT T) $ t end;
   3.210  
   3.211  fun mk_bind (x, f) =
   3.212    let val T as Type ("fun", [_, U]) = fastype_of f
   3.213 @@ -186,16 +186,16 @@
   3.214      Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_bind}, fastype_of x --> T --> U) $ x $ f
   3.215    end;
   3.216  
   3.217 -val mk_sup = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus};
   3.218 +val mk_plus = HOLogic.mk_binop @{const_name Quickcheck_Exhaustive.neg_bound_cps_plus};
   3.219  
   3.220  fun mk_if cond = Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_if},
   3.221 -  HOLogic.boolT --> mk_predT HOLogic.unitT) $ cond;
   3.222 +  HOLogic.boolT --> mk_monadT HOLogic.unitT) $ cond;
   3.223  
   3.224  fun mk_iterate_upto T (f, from, to) = error "not implemented"
   3.225  
   3.226  fun mk_not t =
   3.227    let
   3.228 -    val T = mk_predT HOLogic.unitT
   3.229 +    val T = mk_monadT HOLogic.unitT
   3.230      val pT = @{typ "(unit => Code_Evaluation.term list option) => code_numeral => Code_Evaluation.term list option"}
   3.231    in Const (@{const_name Quickcheck_Exhaustive.neg_bound_cps_not}, pT --> T) $ t end
   3.232  
   3.233 @@ -208,8 +208,8 @@
   3.234  fun mk_map T1 T2 tf tp = error "not implemented"
   3.235  
   3.236  val compfuns = Predicate_Compile_Aux.CompilationFuns
   3.237 -    {mk_predT = mk_predT, dest_predT = dest_predT, mk_bot = mk_bot,
   3.238 -    mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.239 +    {mk_monadT = mk_monadT, dest_monadT = dest_monadT, mk_empty = mk_empty,
   3.240 +    mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
   3.241      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
   3.242  
   3.243  end;
   3.244 @@ -219,13 +219,13 @@
   3.245  struct
   3.246  
   3.247  fun mk_randompredT T =
   3.248 -  @{typ Random.seed} --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_predT T, @{typ Random.seed})
   3.249 +  @{typ Random.seed} --> HOLogic.mk_prodT (Predicate_Comp_Funs.mk_monadT T, @{typ Random.seed})
   3.250  
   3.251  fun dest_randompredT (Type ("fun", [@{typ Random.seed}, Type (@{type_name Product_Type.prod},
   3.252    [Type (@{type_name "Predicate.pred"}, [T]), @{typ Random.seed}])])) = T
   3.253    | dest_randompredT T = raise TYPE ("dest_randompredT", [T], []);
   3.254  
   3.255 -fun mk_bot T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
   3.256 +fun mk_empty T = Const(@{const_name Quickcheck.empty}, mk_randompredT T)
   3.257  
   3.258  fun mk_single t =
   3.259    let               
   3.260 @@ -241,7 +241,7 @@
   3.261      Const (@{const_name Quickcheck.bind}, fastype_of x --> T --> U) $ x $ f
   3.262    end
   3.263  
   3.264 -val mk_sup = HOLogic.mk_binop @{const_name Quickcheck.union}
   3.265 +val mk_plus = HOLogic.mk_binop @{const_name Quickcheck.union}
   3.266  
   3.267  fun mk_if cond = Const (@{const_name Quickcheck.if_randompred},
   3.268    HOLogic.boolT --> mk_randompredT HOLogic.unitT) $ cond;
   3.269 @@ -260,8 +260,8 @@
   3.270    (T1 --> T2) --> mk_randompredT T1 --> mk_randompredT T2) $ tf $ tp
   3.271  
   3.272  val compfuns = Predicate_Compile_Aux.CompilationFuns
   3.273 -    {mk_predT = mk_randompredT, dest_predT = dest_randompredT,
   3.274 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.275 +    {mk_monadT = mk_randompredT, dest_monadT = dest_randompredT,
   3.276 +    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
   3.277      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map};
   3.278  
   3.279  end;
   3.280 @@ -276,7 +276,7 @@
   3.281    Type (@{type_name Option.option}, [Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])) = T
   3.282    | dest_dseqT T = raise TYPE ("dest_dseqT", [T], []);
   3.283  
   3.284 -fun mk_bot T = Const (@{const_name DSequence.empty}, mk_dseqT T);
   3.285 +fun mk_empty T = Const (@{const_name DSequence.empty}, mk_dseqT T);
   3.286  
   3.287  fun mk_single t =
   3.288    let val T = fastype_of t
   3.289 @@ -288,7 +288,7 @@
   3.290      Const (@{const_name DSequence.bind}, fastype_of x --> T --> U) $ x $ f
   3.291    end;
   3.292  
   3.293 -val mk_sup = HOLogic.mk_binop @{const_name DSequence.union};
   3.294 +val mk_plus = HOLogic.mk_binop @{const_name DSequence.union};
   3.295  
   3.296  fun mk_if cond = Const (@{const_name DSequence.if_seq},
   3.297    HOLogic.boolT --> mk_dseqT HOLogic.unitT) $ cond;
   3.298 @@ -302,8 +302,8 @@
   3.299    (T1 --> T2) --> mk_dseqT T1 --> mk_dseqT T2) $ tf $ tp
   3.300  
   3.301  val compfuns = Predicate_Compile_Aux.CompilationFuns
   3.302 -    {mk_predT = mk_dseqT, dest_predT = dest_dseqT,
   3.303 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.304 +    {mk_monadT = mk_dseqT, dest_monadT = dest_dseqT,
   3.305 +    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
   3.306      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   3.307  
   3.308  end;
   3.309 @@ -318,7 +318,7 @@
   3.310      Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])) = T
   3.311    | dest_pos_dseqT T = raise TYPE ("dest_pos_dseqT", [T], []);
   3.312  
   3.313 -fun mk_bot T = Const (@{const_name New_DSequence.pos_empty}, mk_pos_dseqT T);
   3.314 +fun mk_empty T = Const (@{const_name New_DSequence.pos_empty}, mk_pos_dseqT T);
   3.315  
   3.316  fun mk_single t =
   3.317    let
   3.318 @@ -339,7 +339,7 @@
   3.319      Const (@{const_name New_DSequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
   3.320    end;
   3.321  
   3.322 -val mk_sup = HOLogic.mk_binop @{const_name New_DSequence.pos_union};
   3.323 +val mk_plus = HOLogic.mk_binop @{const_name New_DSequence.pos_union};
   3.324  
   3.325  fun mk_if cond = Const (@{const_name New_DSequence.pos_if_seq},
   3.326    HOLogic.boolT --> mk_pos_dseqT HOLogic.unitT) $ cond;
   3.327 @@ -358,13 +358,13 @@
   3.328    (T1 --> T2) --> mk_pos_dseqT T1 --> mk_pos_dseqT T2) $ tf $ tp
   3.329  
   3.330  val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
   3.331 -    {mk_predT = mk_pos_dseqT, dest_predT = dest_pos_dseqT,
   3.332 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.333 +    {mk_monadT = mk_pos_dseqT, dest_monadT = dest_pos_dseqT,
   3.334 +    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
   3.335      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   3.336  
   3.337  val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
   3.338 -    {mk_predT = mk_pos_dseqT, dest_predT = dest_pos_dseqT,
   3.339 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.340 +    {mk_monadT = mk_pos_dseqT, dest_monadT = dest_pos_dseqT,
   3.341 +    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
   3.342      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   3.343  
   3.344  end;
   3.345 @@ -379,7 +379,7 @@
   3.346      Type (@{type_name Lazy_Sequence.lazy_sequence}, [Type (@{type_name Option.option}, [T])])])) = T
   3.347    | dest_neg_dseqT T = raise TYPE ("dest_neg_dseqT", [T], []);
   3.348  
   3.349 -fun mk_bot T = Const (@{const_name New_DSequence.neg_empty}, mk_neg_dseqT T);
   3.350 +fun mk_empty T = Const (@{const_name New_DSequence.neg_empty}, mk_neg_dseqT T);
   3.351  
   3.352  fun mk_single t =
   3.353    let
   3.354 @@ -400,7 +400,7 @@
   3.355      Const (@{const_name New_DSequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
   3.356    end;
   3.357  
   3.358 -val mk_sup = HOLogic.mk_binop @{const_name New_DSequence.neg_union};
   3.359 +val mk_plus = HOLogic.mk_binop @{const_name New_DSequence.neg_union};
   3.360  
   3.361  fun mk_if cond = Const (@{const_name New_DSequence.neg_if_seq},
   3.362    HOLogic.boolT --> mk_neg_dseqT HOLogic.unitT) $ cond;
   3.363 @@ -419,13 +419,13 @@
   3.364    (T1 --> T2) --> mk_neg_dseqT T1 --> mk_neg_dseqT T2) $ tf $ tp
   3.365  
   3.366  val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
   3.367 -    {mk_predT = mk_neg_dseqT, dest_predT = dest_neg_dseqT,
   3.368 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.369 +    {mk_monadT = mk_neg_dseqT, dest_monadT = dest_neg_dseqT,
   3.370 +    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
   3.371      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   3.372  
   3.373  val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
   3.374 -    {mk_predT = mk_neg_dseqT, dest_predT = dest_neg_dseqT,
   3.375 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.376 +    {mk_monadT = mk_neg_dseqT, dest_monadT = dest_neg_dseqT,
   3.377 +    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
   3.378      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   3.379  
   3.380  end;
   3.381 @@ -442,7 +442,7 @@
   3.382      Type (@{type_name Lazy_Sequence.lazy_sequence}, [T])])])])])) = T
   3.383    | dest_pos_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
   3.384  
   3.385 -fun mk_bot T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
   3.386 +fun mk_empty T = Const (@{const_name New_Random_Sequence.pos_empty}, mk_pos_random_dseqT T);
   3.387  
   3.388  fun mk_single t =
   3.389    let
   3.390 @@ -463,7 +463,7 @@
   3.391      Const (@{const_name New_Random_Sequence.pos_decr_bind}, fastype_of x --> T --> U) $ x $ f
   3.392    end;
   3.393  
   3.394 -val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union};
   3.395 +val mk_plus = HOLogic.mk_binop @{const_name New_Random_Sequence.pos_union};
   3.396  
   3.397  fun mk_if cond = Const (@{const_name New_Random_Sequence.pos_if_random_dseq},
   3.398    HOLogic.boolT --> mk_pos_random_dseqT HOLogic.unitT) $ cond;
   3.399 @@ -487,13 +487,13 @@
   3.400    (T1 --> T2) --> mk_pos_random_dseqT T1 --> mk_pos_random_dseqT T2) $ tf $ tp
   3.401  
   3.402  val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
   3.403 -    {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT,
   3.404 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.405 +    {mk_monadT = mk_pos_random_dseqT, dest_monadT = dest_pos_random_dseqT,
   3.406 +    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
   3.407      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   3.408  
   3.409  val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
   3.410 -    {mk_predT = mk_pos_random_dseqT, dest_predT = dest_pos_random_dseqT,
   3.411 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.412 +    {mk_monadT = mk_pos_random_dseqT, dest_monadT = dest_pos_random_dseqT,
   3.413 +    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
   3.414      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   3.415  end;
   3.416  
   3.417 @@ -511,7 +511,7 @@
   3.418          [Type (@{type_name Option.option}, [T])])])])])])) = T
   3.419    | dest_neg_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
   3.420  
   3.421 -fun mk_bot T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
   3.422 +fun mk_empty T = Const (@{const_name New_Random_Sequence.neg_empty}, mk_neg_random_dseqT T);
   3.423  
   3.424  fun mk_single t =
   3.425    let
   3.426 @@ -532,7 +532,7 @@
   3.427      Const (@{const_name New_Random_Sequence.neg_decr_bind}, fastype_of x --> T --> U) $ x $ f
   3.428    end;
   3.429  
   3.430 -val mk_sup = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union};
   3.431 +val mk_plus = HOLogic.mk_binop @{const_name New_Random_Sequence.neg_union};
   3.432  
   3.433  fun mk_if cond = Const (@{const_name New_Random_Sequence.neg_if_random_dseq},
   3.434    HOLogic.boolT --> mk_neg_random_dseqT HOLogic.unitT) $ cond;
   3.435 @@ -554,13 +554,13 @@
   3.436    (T1 --> T2) --> mk_neg_random_dseqT T1 --> mk_neg_random_dseqT T2) $ tf $ tp
   3.437  
   3.438  val depth_limited_compfuns = Predicate_Compile_Aux.CompilationFuns
   3.439 -    {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT,
   3.440 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_decr_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.441 +    {mk_monadT = mk_neg_random_dseqT, dest_monadT = dest_neg_random_dseqT,
   3.442 +    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_decr_bind, mk_plus = mk_plus, mk_if = mk_if,
   3.443      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   3.444  
   3.445  val depth_unlimited_compfuns = Predicate_Compile_Aux.CompilationFuns
   3.446 -    {mk_predT = mk_neg_random_dseqT, dest_predT = dest_neg_random_dseqT,
   3.447 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.448 +    {mk_monadT = mk_neg_random_dseqT, dest_monadT = dest_neg_random_dseqT,
   3.449 +    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
   3.450      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   3.451  
   3.452  end;
   3.453 @@ -577,7 +577,7 @@
   3.454    Type (@{type_name Product_Type.prod}, [T, @{typ Random.seed}])])])])) = DSequence_CompFuns.dest_dseqT T
   3.455    | dest_random_dseqT T = raise TYPE ("dest_random_dseqT", [T], []);
   3.456  
   3.457 -fun mk_bot T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
   3.458 +fun mk_empty T = Const (@{const_name Random_Sequence.empty}, mk_random_dseqT T);
   3.459  
   3.460  fun mk_single t =
   3.461    let
   3.462 @@ -591,7 +591,7 @@
   3.463      Const (@{const_name Random_Sequence.bind}, fastype_of x --> T --> U) $ x $ f
   3.464    end;
   3.465  
   3.466 -val mk_sup = HOLogic.mk_binop @{const_name Random_Sequence.union};
   3.467 +val mk_plus = HOLogic.mk_binop @{const_name Random_Sequence.union};
   3.468  
   3.469  fun mk_if cond = Const (@{const_name Random_Sequence.if_random_dseq},
   3.470    HOLogic.boolT --> mk_random_dseqT HOLogic.unitT) $ cond;
   3.471 @@ -607,8 +607,8 @@
   3.472    (T1 --> T2) --> mk_random_dseqT T1 --> mk_random_dseqT T2) $ tf $ tp
   3.473  
   3.474  val compfuns = Predicate_Compile_Aux.CompilationFuns
   3.475 -    {mk_predT = mk_random_dseqT, dest_predT = dest_random_dseqT,
   3.476 -    mk_bot = mk_bot, mk_single = mk_single, mk_bind = mk_bind, mk_sup = mk_sup, mk_if = mk_if,
   3.477 +    {mk_monadT = mk_random_dseqT, dest_monadT = dest_random_dseqT,
   3.478 +    mk_empty = mk_empty, mk_single = mk_single, mk_bind = mk_bind, mk_plus = mk_plus, mk_if = mk_if,
   3.479      mk_iterate_upto = mk_iterate_upto, mk_not = mk_not, mk_map = mk_map}
   3.480  
   3.481  end;
     4.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 11 10:40:36 2011 +0100
     4.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 11 12:10:49 2011 +0100
     4.3 @@ -312,11 +312,11 @@
     4.4      let
     4.5        val [depth] = additional_arguments
     4.6        val (_, Ts) = split_modeT mode (binder_types T)
     4.7 -      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
     4.8 +      val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts)
     4.9        val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
    4.10      in
    4.11        if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
    4.12 -        $ mk_bot compfuns (dest_predT compfuns T')
    4.13 +        $ mk_empty compfuns (dest_monadT compfuns T')
    4.14          $ compilation
    4.15      end,
    4.16    transform_additional_arguments =
    4.17 @@ -337,7 +337,7 @@
    4.18    mk_random = (fn T => fn additional_arguments =>
    4.19    list_comb (Const(@{const_name Quickcheck.iter},
    4.20    [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
    4.21 -    Predicate_Comp_Funs.mk_predT T), additional_arguments)),
    4.22 +    Predicate_Comp_Funs.mk_monadT T), additional_arguments)),
    4.23    modify_funT = (fn T =>
    4.24      let
    4.25        val (Ts, U) = strip_type T
    4.26 @@ -363,7 +363,7 @@
    4.27    mk_random = (fn T => fn additional_arguments =>
    4.28    list_comb (Const(@{const_name Quickcheck.iter},
    4.29    [@{typ code_numeral}, @{typ code_numeral}, @{typ Random.seed}] ---> 
    4.30 -    Predicate_Comp_Funs.mk_predT T), tl additional_arguments)),
    4.31 +    Predicate_Comp_Funs.mk_monadT T), tl additional_arguments)),
    4.32    modify_funT = (fn T =>
    4.33      let
    4.34        val (Ts, U) = strip_type T
    4.35 @@ -383,11 +383,11 @@
    4.36        val depth = hd (additional_arguments)
    4.37        val (_, Ts) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE))
    4.38          mode (binder_types T)
    4.39 -      val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
    4.40 +      val T' = mk_monadT compfuns (HOLogic.mk_tupleT Ts)
    4.41        val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
    4.42      in
    4.43        if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"})
    4.44 -        $ mk_bot compfuns (dest_predT compfuns T')
    4.45 +        $ mk_empty compfuns (dest_monadT compfuns T')
    4.46          $ compilation
    4.47      end,
    4.48    transform_additional_arguments =
    4.49 @@ -658,7 +658,7 @@
    4.50      val name' = singleton (Name.variant_list (name :: names)) "y";
    4.51      val T = HOLogic.mk_tupleT (map fastype_of out_ts);
    4.52      val U = fastype_of success_t;
    4.53 -    val U' = dest_predT compfuns U;
    4.54 +    val U' = dest_monadT compfuns U;
    4.55      val v = Free (name, T);
    4.56      val v' = Free (name', T);
    4.57    in
    4.58 @@ -667,8 +667,8 @@
    4.59          if null eqs'' then success_t
    4.60          else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
    4.61            foldr1 HOLogic.mk_conj eqs'' $ success_t $
    4.62 -            mk_bot compfuns U'),
    4.63 -       (v', mk_bot compfuns U')])
    4.64 +            mk_empty compfuns U'),
    4.65 +       (v', mk_empty compfuns U')])
    4.66    end;
    4.67  
    4.68  fun string_of_tderiv ctxt (t, deriv) = 
    4.69 @@ -928,7 +928,7 @@
    4.70                compile_clause compilation_modifiers ctxt all_vs param_modes additional_arguments
    4.71                  inp (in_ts', out_ts') moded_ps'
    4.72              end
    4.73 -        in SOME (foldr1 (mk_sup compfuns) (map compile_clause' moded_clauses)) end
    4.74 +        in SOME (foldr1 (mk_plus compfuns) (map compile_clause' moded_clauses)) end
    4.75      | compile_switch_tree all_vs ctxt_eqs (Node ((position, switched_clauses), left_clauses)) =
    4.76        let
    4.77          val (i, is) = argument_position_of mode position
    4.78 @@ -943,18 +943,18 @@
    4.79              val args = map2 (curry Free) argnames Ts
    4.80              val pattern = list_comb (Const (c, T), args)
    4.81              val ctxt_eqs' = (inp_var, pattern) :: ctxt_eqs
    4.82 -            val compilation = the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs))
    4.83 +            val compilation = the_default (mk_empty compfuns (HOLogic.mk_tupleT outTs))
    4.84                (compile_switch_tree (argnames @ x :: all_vs) ctxt_eqs' switched)
    4.85          in
    4.86            (pattern, compilation)
    4.87          end
    4.88          val switch = Datatype.make_case ctxt Datatype_Case.Quiet [] inp_var
    4.89            ((map compile_single_case switched_clauses) @
    4.90 -            [(xt, mk_bot compfuns (HOLogic.mk_tupleT outTs))])
    4.91 +            [(xt, mk_empty compfuns (HOLogic.mk_tupleT outTs))])
    4.92        in
    4.93          case compile_switch_tree all_vs ctxt_eqs left_clauses of
    4.94            NONE => SOME switch
    4.95 -        | SOME left_comp => SOME (mk_sup compfuns (switch, left_comp))
    4.96 +        | SOME left_comp => SOME (mk_plus compfuns (switch, left_comp))
    4.97        end
    4.98    in
    4.99      compile_switch_tree all_vs [] switch_tree
   4.100 @@ -978,11 +978,11 @@
   4.101        (all_vs @ param_vs)
   4.102      val compfuns = Comp_Mod.compfuns compilation_modifiers
   4.103      fun is_param_type (T as Type ("fun",[_ , T'])) =
   4.104 -      is_some (try (dest_predT compfuns) T) orelse is_param_type T'
   4.105 -      | is_param_type T = is_some (try (dest_predT compfuns) T)
   4.106 +      is_some (try (dest_monadT compfuns) T) orelse is_param_type T'
   4.107 +      | is_param_type T = is_some (try (dest_monadT compfuns) T)
   4.108      val (inpTs, outTs) = split_map_modeT (fn m => fn T => (SOME (funT_of compfuns m T), NONE)) mode
   4.109        (binder_types T)
   4.110 -    val predT = mk_predT compfuns (HOLogic.mk_tupleT outTs)
   4.111 +    val predT = mk_monadT compfuns (HOLogic.mk_tupleT outTs)
   4.112      val funT = Comp_Mod.funT_of compilation_modifiers mode T
   4.113      val (in_ts, _) = fold_map (fold_map_aterms_prodT (curry HOLogic.mk_prod)
   4.114        (fn T => fn (param_vs, names) =>
   4.115 @@ -998,7 +998,7 @@
   4.116      val param_modes = param_vs ~~ ho_arg_modes_of mode
   4.117      val compilation =
   4.118        if detect_switches options then
   4.119 -        the_default (mk_bot compfuns (HOLogic.mk_tupleT outTs))
   4.120 +        the_default (mk_empty compfuns (HOLogic.mk_tupleT outTs))
   4.121            (compile_switch compilation_modifiers ctxt all_vs param_modes additional_arguments mode
   4.122              in_ts' outTs (mk_switch_tree ctxt mode moded_cls))
   4.123        else
   4.124 @@ -1010,9 +1010,9 @@
   4.125          in
   4.126            Comp_Mod.wrap_compilation compilation_modifiers compfuns s T mode additional_arguments
   4.127              (if null cl_ts then
   4.128 -              mk_bot compfuns (HOLogic.mk_tupleT outTs)
   4.129 +              mk_empty compfuns (HOLogic.mk_tupleT outTs)
   4.130              else
   4.131 -              foldr1 (mk_sup compfuns) cl_ts)
   4.132 +              foldr1 (mk_plus compfuns) cl_ts)
   4.133          end
   4.134      val fun_const =
   4.135        Const (function_name_of (Comp_Mod.compilation compilation_modifiers)
   4.136 @@ -1341,7 +1341,7 @@
   4.137                (map (fn i => "x" ^ string_of_int i) (1 upto length Ts))
   4.138              val args = map2 (curry Free) arg_names Ts
   4.139              val predfun = Const (function_name_of Pred ctxt predname full_mode,
   4.140 -              Ts ---> Predicate_Comp_Funs.mk_predT @{typ unit})
   4.141 +              Ts ---> Predicate_Comp_Funs.mk_monadT @{typ unit})
   4.142              val rhs = @{term Predicate.holds} $ (list_comb (predfun, args))
   4.143              val eq_term = HOLogic.mk_Trueprop
   4.144                (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs))
   4.145 @@ -1833,7 +1833,7 @@
   4.146          val (_, outargs) = split_mode (head_mode_of deriv) all_args
   4.147          val t_pred = compile_expr comp_modifiers ctxt
   4.148            (body, deriv) [] additional_arguments;
   4.149 -        val T_pred = dest_predT compfuns (fastype_of t_pred)
   4.150 +        val T_pred = dest_monadT compfuns (fastype_of t_pred)
   4.151          val arrange = HOLogic.tupled_lambda (HOLogic.mk_tuple outargs) output
   4.152        in
   4.153          if null outargs then t_pred else mk_map compfuns T_pred T_compr arrange t_pred
   4.154 @@ -1876,7 +1876,7 @@
   4.155        | New_Pos_Random_DSeq => []
   4.156        | Pos_Generator_DSeq => []
   4.157      val t = analyze_compr ctxt (comp_modifiers, additional_arguments) param_user_modes options t_compr;
   4.158 -    val T = dest_predT compfuns (fastype_of t);
   4.159 +    val T = dest_monadT compfuns (fastype_of t);
   4.160      val t' =
   4.161        if stats andalso compilation = New_Pos_Random_DSeq then
   4.162          mk_map compfuns T (HOLogic.mk_prodT (HOLogic.termT, @{typ code_numeral}))
     5.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Nov 11 10:40:36 2011 +0100
     5.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Nov 11 12:10:49 2011 +0100
     5.3 @@ -186,23 +186,23 @@
     5.4    set_no_higher_order_predicate (!no_higher_order_predicate)
     5.5      (if !debug then debug_options else options)
     5.6  
     5.7 -val mk_predT = Predicate_Compile_Aux.mk_predT Predicate_Comp_Funs.compfuns
     5.8 +val mk_predT = Predicate_Compile_Aux.mk_monadT Predicate_Comp_Funs.compfuns
     5.9  val mk_return' = Predicate_Compile_Aux.mk_single Predicate_Comp_Funs.compfuns
    5.10  val mk_bind' = Predicate_Compile_Aux.mk_bind Predicate_Comp_Funs.compfuns
    5.11  
    5.12 -val mk_randompredT = Predicate_Compile_Aux.mk_predT RandomPredCompFuns.compfuns
    5.13 +val mk_randompredT = Predicate_Compile_Aux.mk_monadT RandomPredCompFuns.compfuns
    5.14  val mk_return = Predicate_Compile_Aux.mk_single RandomPredCompFuns.compfuns
    5.15  val mk_bind = Predicate_Compile_Aux.mk_bind RandomPredCompFuns.compfuns
    5.16  
    5.17  val mk_new_randompredT =
    5.18 -  Predicate_Compile_Aux.mk_predT New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
    5.19 +  Predicate_Compile_Aux.mk_monadT New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
    5.20  val mk_new_return =
    5.21    Predicate_Compile_Aux.mk_single New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
    5.22  val mk_new_bind =
    5.23    Predicate_Compile_Aux.mk_bind New_Pos_Random_Sequence_CompFuns.depth_unlimited_compfuns
    5.24  
    5.25  val mk_new_dseqT =
    5.26 -  Predicate_Compile_Aux.mk_predT New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
    5.27 +  Predicate_Compile_Aux.mk_monadT New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
    5.28  val mk_gen_return =
    5.29    Predicate_Compile_Aux.mk_single New_Pos_DSequence_CompFuns.depth_unlimited_compfuns
    5.30  val mk_gen_bind =
    5.31 @@ -210,7 +210,7 @@
    5.32    
    5.33  
    5.34  val mk_cpsT =
    5.35 -  Predicate_Compile_Aux.mk_predT Pos_Bounded_CPS_Comp_Funs.compfuns
    5.36 +  Predicate_Compile_Aux.mk_monadT Pos_Bounded_CPS_Comp_Funs.compfuns
    5.37  val mk_cps_return =
    5.38    Predicate_Compile_Aux.mk_single Pos_Bounded_CPS_Comp_Funs.compfuns
    5.39  val mk_cps_bind =