src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
changeset 55480 59cc4a8bc28a
parent 55471 198498f861ee
child 55483 f223445a4d0c
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 15:03:23 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Feb 14 15:03:24 2014 +0100
     1.3 @@ -65,7 +65,7 @@
     1.4       * (typ list list * typ list list list list * term list list
     1.5          * term list list list list) list option
     1.6       * (string * term list * term list list
     1.7 -        * ((term list list * term list list list) * (typ list * typ list list)) list) option)
     1.8 +        * ((term list list * term list list list) * typ list) list) option)
     1.9      * Proof.context
    1.10    val mk_iter_fun_arg_types: typ list list list -> int list -> int list list -> term ->
    1.11      typ list list list list
    1.12 @@ -77,7 +77,7 @@
    1.13      (string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
    1.14      (term list * thm list) * Proof.context
    1.15    val define_coiters: string list -> string * term list * term list list
    1.16 -    * ((term list list * term list list list) * (typ list * typ list list)) list ->
    1.17 +    * ((term list list * term list list list) * typ list) list ->
    1.18      (string -> binding) -> typ list -> typ list -> term list -> Proof.context ->
    1.19      (term list * thm list) * Proof.context
    1.20    val derive_induct_iters_thms_for_types: BNF_Def.bnf list ->
    1.21 @@ -87,7 +87,7 @@
    1.22      thm list list -> local_theory -> lfp_sugar_thms
    1.23    val derive_coinduct_coiters_thms_for_types: BNF_Def.bnf list ->
    1.24      string * term list * term list list * ((term list list * term list list list)
    1.25 -      * (typ list * typ list list)) list ->
    1.26 +      * typ list) list ->
    1.27      thm -> thm list -> thm list -> thm list list -> BNF_Def.bnf list -> typ list -> typ list ->
    1.28      typ list -> typ list list list -> int list list -> int list list -> int list -> thm list list ->
    1.29      Ctr_Sugar.ctr_sugar list -> term list list -> thm list list -> (thm list -> thm list) ->
    1.30 @@ -443,9 +443,8 @@
    1.31        let
    1.32          val fun_Ts = map get_Ts dtor_coiter_fun_Tss;
    1.33          val (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts) = mk_coiter_fun_arg_types0 ctr_Tsss Cs ns fun_Ts;
    1.34 -        val pf_Tss = map3 flat_corec_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
    1.35        in
    1.36 -        (q_Tssss, f_Tsss, f_Tssss, (f_sum_prod_Ts, pf_Tss))
    1.37 +        (q_Tssss, f_Tsss, f_Tssss, f_sum_prod_Ts)
    1.38        end;
    1.39  
    1.40      val (r_Tssss, g_Tsss, g_Tssss, unfold_types) = mk_types un_fold_of;
    1.41 @@ -537,7 +536,7 @@
    1.42    let
    1.43      val nn = length fpTs;
    1.44  
    1.45 -    val fpT_to_C as Type (_, [fpT, _]) = snd (strip_typeN nn (fastype_of (hd ctor_iters)));
    1.46 +    val Type (_, [fpT, _]) = snd (strip_typeN nn (fastype_of (hd ctor_iters)));
    1.47  
    1.48      fun generate_iter pre (_, _, fss, xssss) ctor_iter =
    1.49        (mk_binding pre,
    1.50 @@ -552,9 +551,9 @@
    1.51    let
    1.52      val nn = length fpTs;
    1.53  
    1.54 -    val C_to_fpT as Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters)));
    1.55 +    val Type (_, [_, fpT]) = snd (strip_typeN nn (fastype_of (hd dtor_coiters)));
    1.56  
    1.57 -    fun generate_coiter pre ((pfss, cqfsss), (f_sum_prod_Ts, pf_Tss)) dtor_coiter =
    1.58 +    fun generate_coiter pre ((pfss, cqfsss), f_sum_prod_Ts) dtor_coiter =
    1.59        (mk_binding pre,
    1.60         fold_rev (fold_rev Term.lambda) pfss (Term.list_comb (dtor_coiter,
    1.61           map4 mk_preds_getterss_join cs cpss f_sum_prod_Ts cqfsss)));