src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 52898 2af1caada147
parent 52872 fd14b0ead643
child 52899 3ff23987f316
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Aug 07 15:43:58 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Aug 07 17:23:40 2013 +0200
     1.3 @@ -45,7 +45,8 @@
     1.4    val mk_iter_fun_arg_types: typ list -> int list -> int list list -> term ->
     1.5      typ list list list list
     1.6    val mk_coiter_fun_arg_types: typ list -> int list -> int list list -> term ->
     1.7 -    typ list list list list * typ list list list * typ list list list list * typ list
     1.8 +    typ list list
     1.9 +    * (typ list list list list * typ list list list * typ list list list list * typ list)
    1.10    val define_iters: string list ->
    1.11      (typ list list * typ list list list list * term list list * term list list list list) list ->
    1.12      (string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
    1.13 @@ -382,13 +383,15 @@
    1.14      (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts)
    1.15    end;
    1.16  
    1.17 -fun mk_coiter_fun_arg_types Cs ns mss =
    1.18 -  mk_fp_iter_fun_types
    1.19 -  #> mk_coiter_fun_arg_types0 Cs ns mss;
    1.20 +fun mk_coiter_p_pred_types Cs ns = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
    1.21 +
    1.22 +fun mk_coiter_fun_arg_types Cs ns mss dtor_coiter =
    1.23 +  (mk_coiter_p_pred_types Cs ns,
    1.24 +   mk_fp_iter_fun_types dtor_coiter |> mk_coiter_fun_arg_types0 Cs ns mss);
    1.25  
    1.26  fun mk_coiters_args_types Cs ns mss dtor_coiter_fun_Tss lthy =
    1.27    let
    1.28 -    val p_Tss = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_pred1T) ns Cs;
    1.29 +    val p_Tss = mk_coiter_p_pred_types Cs ns;
    1.30  
    1.31      fun mk_types get_Ts =
    1.32        let