src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 55819 e21d83c8e1c7
parent 55810 63d63d854fae
child 55854 ee270328a781
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Sat Mar 01 17:08:39 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Sat Mar 01 20:40:31 2014 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4    end;
     1.5  
     1.6  fun construct_mutualized_fp fp fpTs (fp_sugars : fp_sugar list) bs resBs (resDs, Dss) bnfs
     1.7 -    absT_infos lthy =
     1.8 +    (absT_infos : absT_info list) lthy =
     1.9    let
    1.10      fun of_fp_res get =
    1.11        map (fn {fp_res, fp_res_index, ...} => nth (get fp_res) fp_res_index) fp_sugars;
    1.12 @@ -122,13 +122,10 @@
    1.13      val xTs = map (domain_type o fastype_of) xtors;
    1.14      val yTs = map (domain_type o fastype_of) xtor's;
    1.15  
    1.16 -    fun abs_of allAs Ds bnf = mk_abs (mk_T_of_bnf Ds allAs bnf) o #abs;
    1.17 -    fun rep_of absAT = mk_rep absAT o #rep;
    1.18 -
    1.19 -    val absAs = map3 (abs_of allAs) Dss bnfs absT_infos;
    1.20 -    val absBs = map3 (abs_of allBs) Dss bnfs absT_infos;
    1.21 -    val fp_repAs = map2 rep_of absATs fp_absT_infos;
    1.22 -    val fp_repBs = map2 rep_of absBTs fp_absT_infos;
    1.23 +    val absAs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss;
    1.24 +    val absBs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss;
    1.25 +    val fp_repAs = map2 mk_rep absATs fp_reps;
    1.26 +    val fp_repBs = map2 mk_rep absBTs fp_reps;
    1.27  
    1.28      val (((((phis, phis'), pre_phis), xs), ys), names_lthy) = names_lthy
    1.29        |> mk_Frees' "R" phiTs