src/HOL/Library/Predicate_Compile_Alternative_Defs.thy

   val ooi = Fun (Output, Fun (Output, Fun (Input, Bool)))
   val plus_nat = Core_Data.functional_compilation @{const_name plus} iio
   val minus_nat = Core_Data.functional_compilation @{const_name "minus"} iio
   fun subtract_nat compfuns (_ : typ) =
     let
-      val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
+      val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
     in
       absdummy @{typ nat} (absdummy @{typ nat}
         (Const (@{const_name "If"}, @{typ bool} --> T --> T --> T) $
           (@{term "op > :: nat => nat => bool"} $ Bound 1 $ Bound 0) $
-          Predicate_Compile_Aux.mk_bot compfuns @{typ nat} $
+          Predicate_Compile_Aux.mk_empty compfuns @{typ nat} $
           Predicate_Compile_Aux.mk_single compfuns
           (@{term "op - :: nat => nat => nat"} $ Bound 0 $ Bound 1)))
     end
   fun enumerate_addups_nat compfuns (_ : typ) =
     absdummy @{typ nat} (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ "nat * nat"}

       (@{term "op - :: nat => nat => nat"} $ Bound 1 $ (@{term "Code_Numeral.nat_of"} $ Bound 0))),
       @{term "0 :: code_numeral"}, @{term "Code_Numeral.of_nat"} $ Bound 0))
   fun enumerate_nats compfuns  (_ : typ) =
     let
       val (single_const, _) = strip_comb (Predicate_Compile_Aux.mk_single compfuns @{term "0 :: nat"})
-      val T = Predicate_Compile_Aux.mk_predT compfuns @{typ nat}
+      val T = Predicate_Compile_Aux.mk_monadT compfuns @{typ nat}
     in
       absdummy @{typ nat} (absdummy @{typ nat}
         (Const (@{const_name If}, @{typ bool} --> T --> T --> T) $
           (@{term "op = :: nat => nat => bool"} $ Bound 0 $ @{term "0::nat"}) $
           (Predicate_Compile_Aux.mk_iterate_upto compfuns @{typ nat} (@{term "Code_Numeral.nat_of"},