src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
changeset 55573 6a1cbddebf86
parent 55571 a6153343c44f
child 55575 a5e33e18fb5c
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 19 17:16:40 2014 +1100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 19 08:33:59 2014 +0100
     1.3 @@ -342,7 +342,7 @@
     1.4  fun mk_iters_args_types ctr_Tsss Cs ns mss ctor_iter_fun_Tss lthy =
     1.5    let
     1.6      val Css = map2 replicate ns Cs;
     1.7 -    val y_Tsss = map3 mk_iter_fun_arg_types0 ns mss (map un_fold_of ctor_iter_fun_Tss);
     1.8 +    val y_Tsss = map3 mk_iter_fun_arg_types ns mss (map un_fold_of ctor_iter_fun_Tss);
     1.9      val g_Tss = map2 (fn C => map (fn y_Ts => y_Ts ---> C)) Cs y_Tsss;
    1.10  
    1.11      val ((gss, ysss), lthy) =