src/HOL/Tools/BNF/bnf_fp_n2m.ML
changeset 58634 9f10d82e8188
parent 58585 efc8b2c54a38
child 59049 0d1bfc982501
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Oct 08 14:34:30 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Oct 08 17:09:07 2014 +0200
     1.3 @@ -125,8 +125,8 @@
     1.4      val xTs = map (domain_type o fastype_of) xtors;
     1.5      val yTs = map (domain_type o fastype_of) xtor's;
     1.6  
     1.7 -    val absAs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss;
     1.8 -    val absBs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss;
     1.9 +    val absAs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss;
    1.10 +    val absBs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss;
    1.11      val fp_repAs = map2 mk_rep absATs fp_reps;
    1.12      val fp_repBs = map2 mk_rep absBTs fp_reps;
    1.13  
    1.14 @@ -186,7 +186,7 @@
    1.15      val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs;
    1.16  
    1.17      val xtor_rel_co_induct =
    1.18 -      mk_xtor_rel_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys
    1.19 +      mk_xtor_rel_co_induct_thm fp (@{map 3} cast castAs castBs pre_rels) pre_phis rels phis xs ys
    1.20          xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs
    1.21            rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos)
    1.22          lthy;
    1.23 @@ -268,7 +268,7 @@
    1.24          val subst = Term.typ_subst_atomic fold_thetaAs;
    1.25  
    1.26          fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT;
    1.27 -        val mk_fp_absT_repTs = map5 mk_fp_absT_repT fp_repTs fp_absTs absTs repTs;
    1.28 +        val mk_fp_absT_repTs = @{map 5} mk_fp_absT_repT fp_repTs fp_absTs absTs repTs;
    1.29  
    1.30          val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs);
    1.31  
    1.32 @@ -411,7 +411,7 @@
    1.33                  fp_abs fp_rep abs rep rhs)
    1.34            end;
    1.35  
    1.36 -        val goals = map8 mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps;
    1.37 +        val goals = @{map 8} mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps;
    1.38  
    1.39          val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
    1.40          val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);