added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
authorwenzelm
Wed Oct 08 17:09:07 2014 +0200 (2014-10-08)
changeset 586349f10d82e8188
parent 58633 8529745af3dc
child 58635 010b610eb55d
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
NEWS
src/HOL/Library/bnf_lfp_countable.ML
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_compat.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
src/HOL/Tools/BNF/bnf_util.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Lifting/lifting_bnf.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_util.ML
src/HOL/Tools/SMT/smt_datatypes.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
src/HOL/Tools/coinduction.ML
src/Pure/ML/ml_antiquotations.ML
     1.1 --- a/NEWS	Wed Oct 08 14:34:30 2014 +0200
     1.2 +++ b/NEWS	Wed Oct 08 17:09:07 2014 +0200
     1.3 @@ -137,6 +137,9 @@
     1.4  * Tactical PARALLEL_ALLGOALS is the most common way to refer to
     1.5  PARALLEL_GOALS.
     1.6  
     1.7 +* Basic combinators map, fold, fold_map, split_list are available as
     1.8 +parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
     1.9 +
    1.10  
    1.11  *** System ***
    1.12  
     2.1 --- a/src/HOL/Library/bnf_lfp_countable.ML	Wed Oct 08 14:34:30 2014 +0200
     2.2 +++ b/src/HOL/Library/bnf_lfp_countable.ML	Wed Oct 08 17:09:07 2014 +0200
     2.3 @@ -58,7 +58,7 @@
     2.4  
     2.5  fun mk_encode_injectives_tac ctxt ns induct nchotomys injectss recss map_comps' inj_map_strongs' =
     2.6    HEADGOAL (rtac induct) THEN
     2.7 -  EVERY (map4 (fn n => fn nchotomy => fn injects => fn recs =>
     2.8 +  EVERY (@{map 4} (fn n => fn nchotomy => fn injects => fn recs =>
     2.9        mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs')
    2.10      ns nchotomys injectss recss);
    2.11  
    2.12 @@ -166,7 +166,7 @@
    2.13  
    2.14        val (xs, names_ctxt) = ctxt |> mk_Frees "x" fpTs;
    2.15  
    2.16 -      val conjuncts = map3 mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0);
    2.17 +      val conjuncts = @{map 3} mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0);
    2.18        val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj conjuncts);
    2.19      in
    2.20        Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
     3.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Wed Oct 08 14:34:30 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Wed Oct 08 17:09:07 2014 +0200
     3.3 @@ -154,12 +154,12 @@
     3.4        ||>> mk_Frees "A" (map HOLogic.mk_setT As)
     3.5        ||>> mk_Frees "x" As;
     3.6  
     3.7 -    val CAs = map3 mk_T_of_bnf Dss Ass_repl inners;
     3.8 +    val CAs = @{map 3} mk_T_of_bnf Dss Ass_repl inners;
     3.9      val CCA = mk_T_of_bnf oDs CAs outer;
    3.10 -    val CBs = map3 mk_T_of_bnf Dss Bss_repl inners;
    3.11 +    val CBs = @{map 3} mk_T_of_bnf Dss Bss_repl inners;
    3.12      val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer;
    3.13 -    val inner_setss = map3 mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners;
    3.14 -    val inner_bds = map3 mk_bd_of_bnf Dss Ass_repl inners;
    3.15 +    val inner_setss = @{map 3} mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners;
    3.16 +    val inner_bds = @{map 3} mk_bd_of_bnf Dss Ass_repl inners;
    3.17      val outer_bd = mk_bd_of_bnf oDs CAs outer;
    3.18  
    3.19      (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*)
    3.20 @@ -280,7 +280,7 @@
    3.21            val single_set_bd_thmss =
    3.22              map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
    3.23          in
    3.24 -          map3 (fn set'_eq_set => fn set_alt => fn single_set_bds => fn ctxt =>
    3.25 +          @{map 3} (fn set'_eq_set => fn set_alt => fn single_set_bds => fn ctxt =>
    3.26              mk_comp_set_bd_tac ctxt set'_eq_set bd_ordIso_natLeq_thm_opt set_alt single_set_bds)
    3.27            set'_eq_sets set_alt_thms single_set_bd_thmss
    3.28          end;
    3.29 @@ -320,7 +320,7 @@
    3.30      val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
    3.31  
    3.32      val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)))
    3.33 -      (map3 (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As))
    3.34 +      (@{map 3} (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As))
    3.35          Dss inwitss inners);
    3.36  
    3.37      val inner_witsss = map (map (nth inner_witss) o fst) outer_wits;
    3.38 @@ -637,7 +637,7 @@
    3.39      val before_kill_dest = map2 append kill_poss live_poss;
    3.40      val kill_ns = map length kill_poss;
    3.41      val (inners', accum') =
    3.42 -      fold_map5 (fn i => permute_and_kill (qualify i))
    3.43 +      @{fold_map 5} (fn i => permute_and_kill (qualify i))
    3.44          (if length bnfs = 1 then [0] else (1 upto length bnfs))
    3.45          kill_ns before_kill_src before_kill_dest bnfs accum;
    3.46  
    3.47 @@ -649,7 +649,7 @@
    3.48      val after_lift_src = map2 append new_poss old_poss;
    3.49      val lift_ns = map (fn xs => length As - length xs) Ass';
    3.50    in
    3.51 -    ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i))
    3.52 +    ((kill_poss, As), @{fold_map 5} (fn i => lift_and_permute (qualify i))
    3.53        (if length bnfs = 1 then [0] else 1 upto length bnfs)
    3.54        lift_ns after_lift_src after_lift_dest inners' accum')
    3.55    end;
    3.56 @@ -667,7 +667,7 @@
    3.57      val ((kill_poss, As), (inners', ((cache', unfold_set'), lthy'))) =
    3.58        normalize_bnfs qualify Ass Ds flatten_tyargs inners accum;
    3.59  
    3.60 -    val Ds = oDs @ flat (map3 (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss);
    3.61 +    val Ds = oDs @ flat (@{map 3} (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss);
    3.62      val As = map TFree As;
    3.63    in
    3.64      apfst (rpair (Ds, As))
    3.65 @@ -931,7 +931,7 @@
    3.66              val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
    3.67              val ((inners, (Dss, Ass)), (accum', lthy')) =
    3.68                apfst (apsnd split_list o split_list)
    3.69 -                (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) flatten_tyargs Xs Ds0)
    3.70 +                (@{fold_map 2} (fn i => bnf_of_typ Smart_Inline (qualify i) flatten_tyargs Xs Ds0)
    3.71                  (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' accum);
    3.72            in
    3.73              compose_bnf const_policy qualify flatten_tyargs bnf inners oDs Dss Ass (accum', lthy')
     4.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Oct 08 14:34:30 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Wed Oct 08 17:09:07 2014 +0200
     4.3 @@ -864,7 +864,7 @@
     4.4      val CA = mk_bnf_T Ds As Calpha;
     4.5      val CR = mk_bnf_T Ds RTs Calpha;
     4.6      val setRs =
     4.7 -      map3 (fn R => fn T => fn U =>
     4.8 +      @{map 3} (fn R => fn T => fn U =>
     4.9            HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split R) Rs As Bs;
    4.10  
    4.11      (*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO
    4.12 @@ -1057,7 +1057,7 @@
    4.13  
    4.14      val map_cong0_goal =
    4.15        let
    4.16 -        val prems = map4 (mk_map_cong_prem Logic.mk_implies x) zs bnf_sets_As fs fs_copy;
    4.17 +        val prems = @{map 4} (mk_map_cong_prem Logic.mk_implies x) zs bnf_sets_As fs fs_copy;
    4.18          val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
    4.19            Term.list_comb (bnf_map_AsBs, fs_copy) $ x);
    4.20        in
    4.21 @@ -1074,7 +1074,7 @@
    4.22              fold_rev Logic.all fs (mk_Trueprop_eq (set_comp_map, image_comp_set))
    4.23            end;
    4.24        in
    4.25 -        map3 mk_goal bnf_sets_As bnf_sets_Bs fs
    4.26 +        @{map 3} mk_goal bnf_sets_As bnf_sets_Bs fs
    4.27        end;
    4.28  
    4.29      val card_order_bd_goal = HOLogic.mk_Trueprop (mk_card_order bnf_bd_As);
    4.30 @@ -1185,7 +1185,7 @@
    4.31          fun mk_map_cong mk_implies () =
    4.32            let
    4.33              val prem0 = mk_Trueprop_eq (x, x_copy);
    4.34 -            val prems = map4 (mk_map_cong_prem mk_implies x_copy) zs bnf_sets_As fs fs_copy;
    4.35 +            val prems = @{map 4} (mk_map_cong_prem mk_implies x_copy) zs bnf_sets_As fs fs_copy;
    4.36              val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
    4.37                Term.list_comb (bnf_map_AsBs, fs_copy) $ x_copy);
    4.38              val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy)
    4.39 @@ -1364,7 +1364,7 @@
    4.40                    (mk_Ball (setB $ y) (Term.absfree (dest_Free b)
    4.41                      (HOLogic.mk_imp (R $ a $ b, S $ a $ b))))));
    4.42              val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) $ x $ y) ::
    4.43 -              map6 mk_prem bnf_sets_As bnf_sets_Bs Rs Rs_copy zs ys;
    4.44 +              @{map 6} mk_prem bnf_sets_As bnf_sets_Bs Rs Rs_copy zs ys;
    4.45              val concl = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs_copy) $ x $ y);
    4.46            in
    4.47              Goal.prove_sorry lthy [] []
    4.48 @@ -1389,9 +1389,9 @@
    4.49                [Term.list_comb (relCsBs, S_CsBs) $ (Term.list_comb (bnf_map_AsCs, is) $ x) $ y,
    4.50                 Term.list_comb (relAsCs, S_AsCs) $ x $ (Term.list_comb (bnf_map_BsCs, gs) $ y)];
    4.51              val rhss =
    4.52 -              [Term.list_comb (rel, map3 (fn f => fn P => fn T =>
    4.53 +              [Term.list_comb (rel, @{map 3} (fn f => fn P => fn T =>
    4.54                   mk_vimage2p f (HOLogic.id_const T) $ P) is S_CsBs Bs') $ x $ y,
    4.55 -               Term.list_comb (rel, map3 (fn f => fn P => fn T =>
    4.56 +               Term.list_comb (rel, @{map 3} (fn f => fn P => fn T =>
    4.57                   mk_vimage2p (HOLogic.id_const T) f $ P) gs S_AsCs As') $ x $ y];
    4.58              val goals = map2 mk_goal lhss rhss;
    4.59            in
    4.60 @@ -1451,7 +1451,7 @@
    4.61            let
    4.62              val rel_sets = map2 (fn A => fn B => mk_rel 1 [A] [B] @{term rel_set}) As' Bs';
    4.63              val rel_Rs = Term.list_comb (rel, Rs);
    4.64 -            val goals = map4 (fn R => fn rel_set => fn setA => fn setB => HOLogic.mk_Trueprop
    4.65 +            val goals = @{map 4} (fn R => fn rel_set => fn setA => fn setB => HOLogic.mk_Trueprop
    4.66                (mk_rel_fun rel_Rs (rel_set $ R) $ setA $ setB)) Rs rel_sets bnf_sets_As bnf_sets_Bs;
    4.67            in
    4.68              if null goals then []
    4.69 @@ -1468,7 +1468,7 @@
    4.70  
    4.71          fun mk_inj_map_strong () =
    4.72            let
    4.73 -            val assms = map5 (fn setA => fn z => fn f => fn z' => fn f' =>
    4.74 +            val assms = @{map 5} (fn setA => fn z => fn f => fn z' => fn f' =>
    4.75                fold_rev Logic.all [z, z']
    4.76                  (Logic.mk_implies (mk_Trueprop_mem (z, setA $ x),
    4.77                     Logic.mk_implies (mk_Trueprop_mem (z', setA $ x'),
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Oct 08 14:34:30 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Oct 08 17:09:07 2014 +0200
     5.3 @@ -524,7 +524,7 @@
     5.4  
     5.5  fun massage_multi_notes b_names Ts =
     5.6    maps (fn (thmN, thmss, attrs) =>
     5.7 -    map3 (fn b_name => fn Type (T_name, _) => fn thms =>
     5.8 +    @{map 3} (fn b_name => fn Type (T_name, _) => fn thms =>
     5.9          ((Binding.qualify true b_name (Binding.name thmN), attrs T_name), [(thms, [])]))
    5.10        b_names Ts thmss)
    5.11    #> filter_out (null o fst o hd o snd);
    5.12 @@ -788,7 +788,7 @@
    5.13                []
    5.14              else
    5.15                [mk_Trueprop_eq (build_rel_app names_lthy Rs [] ta tb,
    5.16 -                 (case flat (map5 (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of
    5.17 +                 (case flat (@{map 5} (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of
    5.18                     [] => @{term True}
    5.19                   | conjuncts => Library.foldr1 HOLogic.mk_conj conjuncts))];
    5.20  
    5.21 @@ -824,7 +824,7 @@
    5.22                 names_ctxt)
    5.23              end;
    5.24  
    5.25 -          val (assms, names_lthy) = fold_map2 mk_assms ctrAs ctrBs names_lthy;
    5.26 +          val (assms, names_lthy) = @{fold_map 2} mk_assms ctrAs ctrBs names_lthy;
    5.27            val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis);
    5.28            val thm =
    5.29              Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
    5.30 @@ -968,7 +968,7 @@
    5.31                  ([], ctxt)
    5.32              end;
    5.33            val (goals, names_lthy) = apfst (flat o flat o flat)
    5.34 -            (fold_map2 (fn disc =>
    5.35 +            (@{fold_map 2} (fn disc =>
    5.36                   fold_map (fn sel => fold_map (mk_goal disc sel) setAs))
    5.37                 discAs selAss names_lthy);
    5.38          in
    5.39 @@ -1072,7 +1072,7 @@
    5.40    let
    5.41      val Css = map2 replicate ns Cs;
    5.42      val x_Tssss =
    5.43 -      map6 (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_rec_fun_T =>
    5.44 +      @{map 6} (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_rec_fun_T =>
    5.45            map2 (map2 unzip_recT)
    5.46              ctr_Tss (dest_absumprodT absT repT n ms (domain_type ctor_rec_fun_T)))
    5.47          absTs repTs ns mss ctr_Tsss ctor_rec_fun_Ts;
    5.48 @@ -1100,8 +1100,8 @@
    5.49    let
    5.50      val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss;
    5.51      val g_absTs = map range_type fun_Ts;
    5.52 -    val g_Tsss = map repair_nullary_single_ctr (map5 dest_absumprodT absTs repTs ns mss g_absTs);
    5.53 -    val g_Tssss = map3 (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT)))
    5.54 +    val g_Tsss = map repair_nullary_single_ctr (@{map 5} dest_absumprodT absTs repTs ns mss g_absTs);
    5.55 +    val g_Tssss = @{map 3} (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT)))
    5.56        Cs ctr_Tsss' g_Tsss;
    5.57      val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) g_Tssss;
    5.58    in
    5.59 @@ -1139,10 +1139,10 @@
    5.60          mk_If cq (build_sum_inj Inl_const (fastype_of cg, T) $ cg)
    5.61            (build_sum_inj Inr_const (fastype_of cg', T) $ cg');
    5.62  
    5.63 -    val pgss = map3 flat_corec_preds_predsss_gettersss pss qssss gssss;
    5.64 +    val pgss = @{map 3} flat_corec_preds_predsss_gettersss pss qssss gssss;
    5.65      val cqssss = map2 (map o map o map o rapp) cs qssss;
    5.66      val cgssss = map2 (map o map o map o rapp) cs gssss;
    5.67 -    val cqgsss = map3 (map3 (map3 build_dtor_corec_arg)) g_Tsss cqssss cgssss;
    5.68 +    val cqgsss = @{map 3} (@{map 3} (@{map 3} build_dtor_corec_arg)) g_Tsss cqssss cgssss;
    5.69    in
    5.70      ((x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types)), lthy)
    5.71    end;
    5.72 @@ -1200,7 +1200,7 @@
    5.73    in
    5.74      define_co_rec_as Least_FP Cs fpT (mk_binding recN)
    5.75        (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec,
    5.76 -         map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
    5.77 +         @{map 4} (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
    5.78               mk_case_absumprod ctor_rec_absT rep fs (map (map HOLogic.mk_tuple) xsss)
    5.79                 (map flat_rec_arg_args xsss))
    5.80             ctor_rec_absTs reps fss xssss)))
    5.81 @@ -1213,7 +1213,7 @@
    5.82    in
    5.83      define_co_rec_as Greatest_FP Cs fpT (mk_binding corecN)
    5.84        (fold_rev (fold_rev Term.lambda) pgss (Term.list_comb (dtor_corec,
    5.85 -         map5 mk_preds_getterss_join cs cpss f_absTs abss cqgsss)))
    5.86 +         @{map 5} mk_preds_getterss_join cs cpss f_absTs abss cqgsss)))
    5.87    end;
    5.88  
    5.89  fun postproc_co_induct lthy nn prop prop_conj =
    5.90 @@ -1256,7 +1256,7 @@
    5.91              (HOLogic.mk_Trueprop (build_rel_app names_lthy (Rs @ IRs) fpA_Ts
    5.92                (Term.list_comb (ctrA, argAs)) (Term.list_comb (ctrB, argBs)))));
    5.93        in
    5.94 -        flat (map4 (map4 mk_prem) ctrAss ctrBss ctrAsss ctrBsss)
    5.95 +        flat (@{map 4} (@{map 4} mk_prem) ctrAss ctrBss ctrAsss ctrBsss)
    5.96        end;
    5.97  
    5.98      val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
    5.99 @@ -1354,7 +1354,7 @@
   5.100          fun mk_prem (xs, raw_pprems, concl) =
   5.101            fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl));
   5.102  
   5.103 -        val raw_premss = map4 (map3 o mk_raw_prem) ps ctrss ctr_Tsss ctrXs_Tsss;
   5.104 +        val raw_premss = @{map 4} (@{map 3} o mk_raw_prem) ps ctrss ctr_Tsss ctrXs_Tsss;
   5.105  
   5.106          val goal =
   5.107            Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
   5.108 @@ -1402,9 +1402,9 @@
   5.109              end;
   5.110  
   5.111          val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss;
   5.112 -        val goalss = map5 (map4 o mk_goal) frecs xctrss fss xsss fxsss;
   5.113 +        val goalss = @{map 5} (@{map 4} o mk_goal) frecs xctrss fss xsss fxsss;
   5.114  
   5.115 -        val tacss = map4 (map ooo
   5.116 +        val tacss = @{map 4} (map ooo
   5.117                mk_rec_tac pre_map_defs (fp_nesting_map_ident0s @ live_nesting_map_ident0s) rec_defs)
   5.118              ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss;
   5.119  
   5.120 @@ -1441,7 +1441,7 @@
   5.121  
   5.122      val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
   5.123      val coinduct_conclss =
   5.124 -      map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
   5.125 +      @{map 3} (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
   5.126  
   5.127      val common_coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
   5.128      val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
   5.129 @@ -1506,7 +1506,7 @@
   5.130                   (map2 (build_rel_app lthy (Rs @ IRs) fpA_Ts) selA_ts selB_ts))]);
   5.131  
   5.132          fun mk_prem_concl n discA_ts selA_tss discB_ts selB_tss =
   5.133 -          Library.foldr1 HOLogic.mk_conj (flat (map5 (mk_prem_ctr_concls n)
   5.134 +          Library.foldr1 HOLogic.mk_conj (flat (@{map 5} (mk_prem_ctr_concls n)
   5.135              (1 upto n) discA_ts selA_tss discB_ts selB_tss))
   5.136            handle List.Empty => @{term True};
   5.137  
   5.138 @@ -1514,7 +1514,7 @@
   5.139            fold_rev Logic.all [tA, tB] (Logic.mk_implies (HOLogic.mk_Trueprop (IR $ tA $ tB),
   5.140              HOLogic.mk_Trueprop (mk_prem_concl n discA_ts selA_tss discB_ts selB_tss)));
   5.141        in
   5.142 -        map8 mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss
   5.143 +        @{map 8} mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss
   5.144        end;
   5.145  
   5.146      val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
   5.147 @@ -1632,7 +1632,8 @@
   5.148      fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec =
   5.149        iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]];
   5.150  
   5.151 -    val ctor_dtor_corec_thms = map3 mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms;
   5.152 +    val ctor_dtor_corec_thms =
   5.153 +      @{map 3} mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms;
   5.154  
   5.155      val nn = length pre_bnfs;
   5.156  
   5.157 @@ -1667,10 +1668,10 @@
   5.158  
   5.159      val coinduct_thms_pairs =
   5.160        let
   5.161 -        val uvrs = map3 (fn r => fn u => fn v => r $ u $ v) rs us vs;
   5.162 +        val uvrs = @{map 3} (fn r => fn u => fn v => r $ u $ v) rs us vs;
   5.163          val uv_eqs = map2 (curry HOLogic.mk_eq) us vs;
   5.164          val strong_rs =
   5.165 -          map4 (fn u => fn v => fn uvr => fn uv_eq =>
   5.166 +          @{map 4} (fn u => fn v => fn uvr => fn uv_eq =>
   5.167              fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs;
   5.168  
   5.169          fun build_the_rel rs' T Xs_T =
   5.170 @@ -1686,10 +1687,10 @@
   5.171               []
   5.172             else
   5.173               [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc],
   5.174 -                Library.foldr1 HOLogic.mk_conj (map3 (build_rel_app rs') usels vsels ctrXs_Ts))]);
   5.175 +                Library.foldr1 HOLogic.mk_conj (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]);
   5.176  
   5.177          fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss =
   5.178 -          Library.foldr1 HOLogic.mk_conj (flat (map6 (mk_prem_ctr_concls rs' n)
   5.179 +          Library.foldr1 HOLogic.mk_conj (flat (@{map 6} (mk_prem_ctr_concls rs' n)
   5.180              (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss))
   5.181            handle List.Empty => @{term True};
   5.182  
   5.183 @@ -1699,11 +1700,11 @@
   5.184  
   5.185          val concl =
   5.186            HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   5.187 -            (map3 (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v)))
   5.188 +            (@{map 3} (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v)))
   5.189                 uvrs us vs));
   5.190  
   5.191          fun mk_goal rs' =
   5.192 -          Logic.list_implies (map9 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss
   5.193 +          Logic.list_implies (@{map 9} (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss
   5.194              ctrXs_Tsss, concl);
   5.195  
   5.196          val goals = map mk_goal [rs, strong_rs];
   5.197 @@ -1757,10 +1758,10 @@
   5.198            end;
   5.199  
   5.200          val cqgsss' = map (map (map build_corec)) cqgsss;
   5.201 -        val goalss = map8 (map4 oooo mk_goal) cs cpss gcorecs ns kss ctrss mss cqgsss';
   5.202 +        val goalss = @{map 8} (@{map 4} oooo mk_goal) cs cpss gcorecs ns kss ctrss mss cqgsss';
   5.203  
   5.204          val tacss =
   5.205 -          map4 (map ooo mk_corec_tac corec_defs live_nesting_map_ident0s)
   5.206 +          @{map 4} (map ooo mk_corec_tac corec_defs live_nesting_map_ident0s)
   5.207              ctor_dtor_corec_thms pre_map_defs abs_inverses ctr_defss;
   5.208  
   5.209          fun prove goal tac =
   5.210 @@ -1778,13 +1779,13 @@
   5.211              if n = 1 then @{const True}
   5.212              else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
   5.213  
   5.214 -        val goalss = map6 (map2 oooo mk_goal) cs cpss gcorecs ns kss discss;
   5.215 +        val goalss = @{map 6} (map2 oooo mk_goal) cs cpss gcorecs ns kss discss;
   5.216  
   5.217          fun mk_case_split' cp = Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split};
   5.218  
   5.219          val case_splitss' = map (map mk_case_split') cpss;
   5.220  
   5.221 -        val tacss = map3 (map oo mk_corec_disc_iff_tac) case_splitss' corec_thmss disc_thmsss;
   5.222 +        val tacss = @{map 3} (map oo mk_corec_disc_iff_tac) case_splitss' corec_thmss disc_thmsss;
   5.223  
   5.224          fun prove goal tac =
   5.225            Goal.prove_sorry lthy [] [] goal (tac o #context)
   5.226 @@ -1815,7 +1816,7 @@
   5.227        end;
   5.228  
   5.229      fun mk_corec_sel_thms corec_thmss =
   5.230 -      map3 (map3 (map2 o mk_corec_sel_thm)) corec_thmss selsss sel_thmsss;
   5.231 +      @{map 3} (@{map 3} (map2 o mk_corec_sel_thm)) corec_thmss selsss sel_thmsss;
   5.232  
   5.233      val corec_sel_thmsss = mk_corec_sel_thms corec_thmss;
   5.234    in
   5.235 @@ -1997,7 +1998,7 @@
   5.236          ();
   5.237  
   5.238      val Bs =
   5.239 -      map3 (fn alive => fn A as TFree (_, S) => fn B =>
   5.240 +      @{map 3} (fn alive => fn A as TFree (_, S) => fn B =>
   5.241            if alive then resort_tfree_or_tvar S B else A)
   5.242          (liveness_of_fp_bnf num_As any_fp_bnf) As Bs0;
   5.243  
   5.244 @@ -2044,7 +2045,7 @@
   5.245            #> not (Config.get no_defs_lthy bnf_note_all) ? Binding.conceal;
   5.246  
   5.247          val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
   5.248 -          |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
   5.249 +          |> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs =>
   5.250                Local_Theory.define ((b, mx), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd)
   5.251              ctr_bindings ctr_mixfixes ctr_rhss
   5.252            ||> `Local_Theory.restore;
   5.253 @@ -2103,7 +2104,7 @@
   5.254              val sel_default_eqs = map (prepare_term sel_default_lthy) raw_sel_default_eqs;
   5.255  
   5.256              fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs);
   5.257 -            val ctr_specs = map3 ctr_spec_of disc_bindings ctrs0 sel_bindingss;
   5.258 +            val ctr_specs = @{map 3} ctr_spec_of disc_bindings ctrs0 sel_bindingss;
   5.259  
   5.260              val (ctr_sugar as {case_cong, ...}, lthy') =
   5.261                free_constructors tacss ((((plugins, discs_sels), standard_binding), ctr_specs),
   5.262 @@ -2136,7 +2137,7 @@
   5.263  
   5.264      fun wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types (wrap_one_etc, lthy) =
   5.265        fold_map I wrap_one_etc lthy
   5.266 -      |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list15 o split_list)
   5.267 +      |>> apsnd split_list o apfst (apsnd @{split_list 4} o apfst @{split_list 15} o split_list)
   5.268          o split_list;
   5.269  
   5.270      fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects
   5.271 @@ -2204,7 +2205,7 @@
   5.272              end;
   5.273  
   5.274          val simp_thmss =
   5.275 -          map6 mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss;
   5.276 +          @{map 6} mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss;
   5.277  
   5.278          val common_notes =
   5.279            (if nn > 1 then
   5.280 @@ -2315,8 +2316,8 @@
   5.281            |> split_list;
   5.282  
   5.283          val simp_thmss =
   5.284 -          map6 mk_simp_thms ctr_sugars
   5.285 -            (map3 flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss)
   5.286 +          @{map 6} mk_simp_thms ctr_sugars
   5.287 +            (@{map 3} flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss)
   5.288              map_thmss rel_injectss rel_distinctss set_thmss;
   5.289  
   5.290          val common_notes =
     6.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Oct 08 14:34:30 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Oct 08 17:09:07 2014 +0200
     6.3 @@ -141,7 +141,7 @@
     6.4  
     6.5  fun mk_ctor_iff_dtor_tac ctxt cTs cctor cdtor ctor_dtor dtor_ctor =
     6.6    HEADGOAL (rtac iffI THEN'
     6.7 -    EVERY' (map3 (fn cTs => fn cx => fn th =>
     6.8 +    EVERY' (@{map 3} (fn cTs => fn cx => fn th =>
     6.9        dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
    6.10        SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN'
    6.11        atac) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor]));
    6.12 @@ -212,7 +212,7 @@
    6.13    end;
    6.14  
    6.15  fun mk_corec_disc_iff_tac case_splits' corecs discs ctxt =
    6.16 -  EVERY (map3 (fn case_split_tac => fn corec_thm => fn disc =>
    6.17 +  EVERY (@{map 3} (fn case_split_tac => fn corec_thm => fn disc =>
    6.18        HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [corec_thm] THEN
    6.19        HEADGOAL (asm_simp_tac (ss_only basic_simp_thms ctxt)) THEN
    6.20        (if is_refl disc then all_tac else HEADGOAL (rtac disc)))
    6.21 @@ -277,7 +277,7 @@
    6.22  
    6.23      fun mk_unfold_prop_tac dtor_corec_transfer corec_def =
    6.24        mk_unfold_corec_type_tac dtor_corec_transfer corec_def THEN
    6.25 -      EVERY (map4 mk_unfold_type_tac type_definitions pss qssss gssss);
    6.26 +      EVERY (@{map 4} mk_unfold_type_tac type_definitions pss qssss gssss);
    6.27    in
    6.28      HEADGOAL Goal.conjunction_tac THEN
    6.29      EVERY (map2 mk_unfold_prop_tac dtor_corec_transfers corec_defs)
    6.30 @@ -315,7 +315,7 @@
    6.31       else
    6.32         unfold_thms_tac ctxt ctr_defs) THEN
    6.33      HEADGOAL (rtac ctor_induct') THEN co_induct_inst_as_projs_tac ctxt 0 THEN
    6.34 -    EVERY (map4 (EVERY oooo map3 o
    6.35 +    EVERY (@{map 4} (EVERY oooo @{map 3} o
    6.36          mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps)
    6.37        pre_set_defss mss (unflat mss (1 upto n)) kkss)
    6.38    end;
    6.39 @@ -348,7 +348,7 @@
    6.40      EVERY' ([rtac allI, rtac allI, rtac impI, select_prem_tac nn (dtac meta_spec) kk,
    6.41          dtac meta_spec, dtac meta_mp, atac, rtac exhaust, K (co_induct_inst_as_projs_tac ctxt 0),
    6.42          hyp_subst_tac ctxt] @
    6.43 -      map4 (fn k => fn ctr_def => fn discs => fn sels =>
    6.44 +      @{map 4} (fn k => fn ctr_def => fn discs => fn sels =>
    6.45          EVERY' ([rtac exhaust, K (co_induct_inst_as_projs_tac ctxt 1)] @
    6.46            map2 (fn k' => fn discs' =>
    6.47              if k' = k then
    6.48 @@ -361,7 +361,7 @@
    6.49  fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs fp_abs_inverses abs_inverses
    6.50      dtor_ctors exhausts ctr_defss discsss selsss =
    6.51    HEADGOAL (rtac dtor_coinduct' THEN'
    6.52 -    EVERY' (map10 (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn)
    6.53 +    EVERY' (@{map 10} (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn)
    6.54        (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
    6.55        selsss));
    6.56  
    6.57 @@ -401,7 +401,7 @@
    6.58  fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss
    6.59      dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses nesting_rel_eqs =
    6.60    rtac dtor_rel_coinduct 1 THEN
    6.61 -   EVERY (map11 (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
    6.62 +   EVERY (@{map 11} (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
    6.63       fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse =>
    6.64        (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW
    6.65           (dtac (rotate_prems ~1 (cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct]
    6.66 @@ -420,7 +420,7 @@
    6.67  
    6.68  fun mk_rel_induct0_tac ctxt ctor_rel_induct assms cterms exhausts ctor_defss ctor_injects
    6.69      rel_pre_list_defs Abs_inverses nesting_rel_eqs =
    6.70 -  rtac ctor_rel_induct 1 THEN EVERY (map6 (fn cterm => fn exhaust => fn ctor_defs =>
    6.71 +  rtac ctor_rel_induct 1 THEN EVERY (@{map 6} (fn cterm => fn exhaust => fn ctor_defs =>
    6.72        fn ctor_inject => fn rel_pre_list_def => fn Abs_inverse =>
    6.73          HEADGOAL (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW
    6.74            (rtac (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
     7.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Oct 08 14:34:30 2014 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Oct 08 17:09:07 2014 +0200
     7.3 @@ -125,8 +125,8 @@
     7.4      val xTs = map (domain_type o fastype_of) xtors;
     7.5      val yTs = map (domain_type o fastype_of) xtor's;
     7.6  
     7.7 -    val absAs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss;
     7.8 -    val absBs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss;
     7.9 +    val absAs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss;
    7.10 +    val absBs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss;
    7.11      val fp_repAs = map2 mk_rep absATs fp_reps;
    7.12      val fp_repBs = map2 mk_rep absBTs fp_reps;
    7.13  
    7.14 @@ -186,7 +186,7 @@
    7.15      val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs;
    7.16  
    7.17      val xtor_rel_co_induct =
    7.18 -      mk_xtor_rel_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys
    7.19 +      mk_xtor_rel_co_induct_thm fp (@{map 3} cast castAs castBs pre_rels) pre_phis rels phis xs ys
    7.20          xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs
    7.21            rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos)
    7.22          lthy;
    7.23 @@ -268,7 +268,7 @@
    7.24          val subst = Term.typ_subst_atomic fold_thetaAs;
    7.25  
    7.26          fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT;
    7.27 -        val mk_fp_absT_repTs = map5 mk_fp_absT_repT fp_repTs fp_absTs absTs repTs;
    7.28 +        val mk_fp_absT_repTs = @{map 5} mk_fp_absT_repT fp_repTs fp_absTs absTs repTs;
    7.29  
    7.30          val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs);
    7.31  
    7.32 @@ -411,7 +411,7 @@
    7.33                  fp_abs fp_rep abs rep rhs)
    7.34            end;
    7.35  
    7.36 -        val goals = map8 mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps;
    7.37 +        val goals = @{map 8} mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps;
    7.38  
    7.39          val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
    7.40          val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
     8.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Oct 08 14:34:30 2014 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Oct 08 17:09:07 2014 +0200
     8.3 @@ -205,7 +205,7 @@
     8.4        | freeze_fpTs_call _ _ _ T = T;
     8.5  
     8.6      val ctr_Tsss = map (map binder_types) ctr_Tss;
     8.7 -    val ctrXs_Tsss = map4 (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss;
     8.8 +    val ctrXs_Tsss = @{map 4} (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss;
     8.9      val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss;
    8.10  
    8.11      val ns = map length ctr_Tsss;
    8.12 @@ -261,7 +261,7 @@
    8.13          fun mk_binding b pre = Binding.prefix_name (pre ^ "_") b;
    8.14  
    8.15          val ((co_recs, co_rec_defs), lthy) =
    8.16 -          fold_map2 (fn b =>
    8.17 +          @{fold_map 2} (fn b =>
    8.18                if fp = Least_FP then define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps
    8.19                else define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss)
    8.20              fp_bs xtor_co_recs lthy
    8.21 @@ -340,9 +340,9 @@
    8.22            |> morph_fp_sugar phi;
    8.23  
    8.24          val target_fp_sugars =
    8.25 -          map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
    8.26 -            co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss co_rec_disc_thmss
    8.27 -            co_rec_sel_thmsss fp_sugars0;
    8.28 +          @{map 16} mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss
    8.29 +            ctr_sugars co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss
    8.30 +            co_rec_disc_thmss co_rec_sel_thmsss fp_sugars0;
    8.31  
    8.32          val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
    8.33        in
     9.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Wed Oct 08 14:34:30 2014 +0200
     9.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Wed Oct 08 17:09:07 2014 +0200
     9.3 @@ -32,7 +32,7 @@
     9.4      val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs;
     9.5      val C_IHs = map2 (curry op |>) folded_C_IHs unfolds;
     9.6      val C_IH_monos =
     9.7 -      map3 (fn C_IH => fn mono => fn unfold =>
     9.8 +      @{map 3} (fn C_IH => fn mono => fn unfold =>
     9.9          (mono RSN (2, @{thm vimage2p_mono}), C_IH)
    9.10          |> fp = Greatest_FP ? swap
    9.11          |> op RS
    10.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Oct 08 14:34:30 2014 +0200
    10.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Oct 08 17:09:07 2014 +0200
    10.3 @@ -433,7 +433,7 @@
    10.4    if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs));
    10.5  
    10.6  fun mk_case_absumprod absT rep fs xss xss' =
    10.7 -  HOLogic.mk_comp (mk_case_sumN_balanced (map3 mk_tupled_fun fs (map mk_tuple_balanced xss) xss'),
    10.8 +  HOLogic.mk_comp (mk_case_sumN_balanced (@{map 3} mk_tupled_fun fs (map mk_tuple_balanced xss) xss'),
    10.9      mk_rep absT rep);
   10.10  
   10.11  fun If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
   10.12 @@ -512,7 +512,7 @@
   10.13      fun mk_prem pre_relphi phi x y xtor xtor' =
   10.14        HOLogic.mk_Trueprop (list_all_free [x, y] (flip (curry HOLogic.mk_imp)
   10.15          (pre_relphi $ (dtor xtor x) $ (dtor xtor' y)) (phi $ (ctor xtor x) $ (ctor xtor' y))));
   10.16 -    val prems = map6 mk_prem pre_relphis pre_phis xs ys xtors xtor's;
   10.17 +    val prems = @{map 6} mk_prem pre_relphis pre_phis xs ys xtors xtor's;
   10.18  
   10.19      val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
   10.20        (map2 (flip mk_leq) relphis pre_phis));
   10.21 @@ -531,7 +531,7 @@
   10.22      val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_ophis;
   10.23      fun mk_transfer relphi pre_phi un_fold un_fold' =
   10.24        fold_rev mk_rel_fun arg_rels (flip mk_rel_fun relphi pre_phi) $ un_fold $ un_fold';
   10.25 -    val transfers = map4 mk_transfer relphis pre_ophis un_folds un_folds';
   10.26 +    val transfers = @{map 4} mk_transfer relphis pre_ophis un_folds un_folds';
   10.27  
   10.28      val goal = fold_rev Logic.all (phis @ pre_ophis)
   10.29        (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers));
   10.30 @@ -565,7 +565,7 @@
   10.31      val rewrite1s = mk_rewrites map_cong1s;
   10.32      val rewrite2s = mk_rewrites map_cong2s;
   10.33      val unique_prems =
   10.34 -      map4 (fn xtor_map => fn un_fold => fn rewrite1 => fn rewrite2 =>
   10.35 +      @{map 4} (fn xtor_map => fn un_fold => fn rewrite1 => fn rewrite2 =>
   10.36          mk_trans (rewrite_comp_comp2 OF [xtor_map, un_fold])
   10.37            (mk_trans rewrite1 (mk_sym rewrite2)))
   10.38        xtor_maps xtor_un_folds rewrite1s rewrite2s;
   10.39 @@ -613,7 +613,8 @@
   10.40  
   10.41      val ((bnfs, (deadss, livess)), accum) =
   10.42        apfst (apsnd split_list o split_list)
   10.43 -        (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs
   10.44 +        (@{fold_map 2}
   10.45 +          (fn b => bnf_of_typ Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs
   10.46            ((empty_comp_cache, empty_unfolds), lthy));
   10.47  
   10.48      fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))
   10.49 @@ -631,13 +632,13 @@
   10.50      val ((kill_poss, _), (bnfs', ((_, unfold_set'), lthy'))) =
   10.51        normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs accum;
   10.52  
   10.53 -    val Dss = map3 (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
   10.54 +    val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
   10.55  
   10.56      fun pre_qualify b = Binding.qualify false (Binding.name_of b)
   10.57        #> not (Config.get lthy' bnf_note_all) ? Binding.conceal;
   10.58  
   10.59      val ((pre_bnfs, (deadss, absT_infos)), lthy'') =
   10.60 -      fold_map4 (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
   10.61 +      @{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
   10.62          bs (not (null live_phantoms) :: replicate (nn - 1) false) Dss bnfs' lthy'
   10.63        |>> split_list
   10.64        |>> apsnd split_list;
    11.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Oct 08 14:34:30 2014 +0200
    11.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Oct 08 17:09:07 2014 +0200
    11.3 @@ -138,21 +138,21 @@
    11.4      val sum_sTs = map2 (fn T => fn U => T --> U) activeAs sumFTs;
    11.5  
    11.6      (* terms *)
    11.7 -    val mapsAsAs = map4 mk_map_of_bnf Dss Ass Ass bnfs;
    11.8 -    val mapsAsBs = map4 mk_map_of_bnf Dss Ass Bss bnfs;
    11.9 -    val mapsBsCs' = map4 mk_map_of_bnf Dss Bss Css' bnfs;
   11.10 -    val mapsAsCs' = map4 mk_map_of_bnf Dss Ass Css' bnfs;
   11.11 -    val map_Inls = map4 mk_map_of_bnf Dss Bss (replicate n (passiveAs @ sumBsAs)) bnfs;
   11.12 -    val map_Inls_rev = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ sumBsAs)) Bss bnfs;
   11.13 -    val map_fsts = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Ass bnfs;
   11.14 -    val map_snds = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Bss bnfs;
   11.15 -    fun mk_setss Ts = map3 mk_sets_of_bnf (map (replicate live) Dss)
   11.16 +    val mapsAsAs = @{map 4} mk_map_of_bnf Dss Ass Ass bnfs;
   11.17 +    val mapsAsBs = @{map 4} mk_map_of_bnf Dss Ass Bss bnfs;
   11.18 +    val mapsBsCs' = @{map 4} mk_map_of_bnf Dss Bss Css' bnfs;
   11.19 +    val mapsAsCs' = @{map 4} mk_map_of_bnf Dss Ass Css' bnfs;
   11.20 +    val map_Inls = @{map 4} mk_map_of_bnf Dss Bss (replicate n (passiveAs @ sumBsAs)) bnfs;
   11.21 +    val map_Inls_rev = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ sumBsAs)) Bss bnfs;
   11.22 +    val map_fsts = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Ass bnfs;
   11.23 +    val map_snds = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Bss bnfs;
   11.24 +    fun mk_setss Ts = @{map 3} mk_sets_of_bnf (map (replicate live) Dss)
   11.25        (map (replicate live) (replicate n Ts)) bnfs;
   11.26      val setssAs = mk_setss allAs;
   11.27      val setssAs' = transpose setssAs;
   11.28      val bis_setss = mk_setss (passiveAs @ RTs);
   11.29 -    val relsAsBs = map4 mk_rel_of_bnf Dss Ass Bss bnfs;
   11.30 -    val bds = map3 mk_bd_of_bnf Dss Ass bnfs;
   11.31 +    val relsAsBs = @{map 4} mk_rel_of_bnf Dss Ass Bss bnfs;
   11.32 +    val bds = @{map 3} mk_bd_of_bnf Dss Ass bnfs;
   11.33      val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
   11.34      val sum_bdT = fst (dest_relT (fastype_of sum_bd));
   11.35      val (sum_bdT_params, sum_bdT_params') = `(map TFree) (Term.add_tfreesT sum_bdT []);
   11.36 @@ -244,7 +244,7 @@
   11.37          |> singleton (Proof_Context.export names_lthy lthy)
   11.38        end;
   11.39  
   11.40 -    val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
   11.41 +    val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
   11.42  
   11.43      (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>
   11.44        map id ... id f(m+1) ... f(m+n) x = x*)
   11.45 @@ -253,7 +253,7 @@
   11.46          fun mk_prem set f z z' =
   11.47            HOLogic.mk_Trueprop
   11.48              (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
   11.49 -        val prems = map4 mk_prem (drop m sets) self_fs zs zs';
   11.50 +        val prems = @{map 4} mk_prem (drop m sets) self_fs zs zs';
   11.51          val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
   11.52        in
   11.53          Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
   11.54 @@ -262,7 +262,7 @@
   11.55          |> singleton (Proof_Context.export names_lthy lthy)
   11.56        end;
   11.57  
   11.58 -    val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
   11.59 +    val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
   11.60      val in_mono'_thms = map (fn thm =>
   11.61        (thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos;
   11.62  
   11.63 @@ -271,7 +271,8 @@
   11.64          val prems = map2 (curry mk_Trueprop_eq) yFs yFs_copy;
   11.65          val maps = map (fn mapx => Term.list_comb (mapx, all_gs)) mapsBsCs';
   11.66          val concls =
   11.67 -          map3 (fn x => fn y => fn mapx => mk_Trueprop_eq (mapx $ x, mapx $ y)) yFs yFs_copy maps;
   11.68 +          @{map 3} (fn x => fn y => fn mapx => mk_Trueprop_eq (mapx $ x, mapx $ y))
   11.69 +            yFs yFs_copy maps;
   11.70          val goals = map2 (fn prem => fn concl => Logic.mk_implies (prem, concl)) prems concls;
   11.71        in
   11.72          map (fn goal =>
   11.73 @@ -290,11 +291,11 @@
   11.74      (*forall i = 1 ... n: (\<forall>x \<in> Bi. si \<in> Fi_in UNIV .. UNIV B1 ... Bn)*)
   11.75      val coalg_spec =
   11.76        let
   11.77 -        val ins = map3 mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs;
   11.78 +        val ins = @{map 3} mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs;
   11.79          fun mk_coalg_conjunct B s X z z' =
   11.80            mk_Ball B (Term.absfree z' (HOLogic.mk_mem (s $ z, X)));
   11.81  
   11.82 -        val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_coalg_conjunct Bs ss ins zs zs')
   11.83 +        val rhs = Library.foldr1 HOLogic.mk_conj (@{map 5} mk_coalg_conjunct Bs ss ins zs zs')
   11.84        in
   11.85          fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs
   11.86        end;
   11.87 @@ -328,7 +329,7 @@
   11.88          fun mk_prem x B = mk_Trueprop_mem (x, B);
   11.89          fun mk_concl s x B set = HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) B);
   11.90          val prems = map2 mk_prem zs Bs;
   11.91 -        val conclss = map3 (fn s => fn x => fn sets => map2 (mk_concl s x) Bs (drop m sets))
   11.92 +        val conclss = @{map 3} (fn s => fn x => fn sets => map2 (mk_concl s x) Bs (drop m sets))
   11.93            ss zs setssAs;
   11.94          val goalss = map2 (fn prem => fn concls => map (fn concl =>
   11.95            Logic.list_implies (coalg_prem :: [prem], concl)) concls) prems conclss;
   11.96 @@ -371,8 +372,8 @@
   11.97            mk_Ball B (Term.absfree z' (HOLogic.mk_eq
   11.98              (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ z]), s' $ (f $ z))));
   11.99          val rhs = HOLogic.mk_conj
  11.100 -          (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'),
  11.101 -           Library.foldr1 HOLogic.mk_conj (map7 mk_mor Bs mapsAsBs fs ss s's zs zs'))
  11.102 +          (Library.foldr1 HOLogic.mk_conj (@{map 5} mk_fbetw fs Bs B's zs zs'),
  11.103 +           Library.foldr1 HOLogic.mk_conj (@{map 7} mk_mor Bs mapsAsBs fs ss s's zs zs'))
  11.104        in
  11.105          fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs
  11.106        end;
  11.107 @@ -402,11 +403,11 @@
  11.108          val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
  11.109          fun mk_image_goal f B1 B2 =
  11.110            Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2));
  11.111 -        val image_goals = map3 mk_image_goal fs Bs B's;
  11.112 +        val image_goals = @{map 3} mk_image_goal fs Bs B's;
  11.113          fun mk_elim_goal B mapAsBs f s s' x =
  11.114            Logic.list_implies ([prem, mk_Trueprop_mem (x, B)],
  11.115              mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x)));
  11.116 -        val elim_goals = map6 mk_elim_goal Bs mapsAsBs fs ss s's zs;
  11.117 +        val elim_goals = @{map 6} mk_elim_goal Bs mapsAsBs fs ss s's zs;
  11.118          fun prove goal =
  11.119            Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def))
  11.120            |> Thm.close_derivation
  11.121 @@ -462,7 +463,7 @@
  11.122              (HOLogic.mk_comp (Term.list_comb (mapAsBs, passive_ids @ fs), s),
  11.123              HOLogic.mk_comp (s', f));
  11.124          val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
  11.125 -        val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
  11.126 +        val rhs = Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct mapsAsBs fs ss s's);
  11.127        in
  11.128          Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
  11.129            (K (mk_mor_UNIV_tac morE_thms mor_def))
  11.130 @@ -484,7 +485,7 @@
  11.131  
  11.132      val mor_case_sum_thm =
  11.133        let
  11.134 -        val maps = map3 (fn s => fn sum_s => fn mapx =>
  11.135 +        val maps = @{map 3} (fn s => fn sum_s => fn mapx =>
  11.136            mk_case_sum (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ Inls), s), sum_s))
  11.137            s's sum_ss map_Inls;
  11.138        in
  11.139 @@ -503,7 +504,7 @@
  11.140      val bis_def_bind = (Thm.def_binding bis_bind, []);
  11.141  
  11.142      fun mk_bis_le_conjunct R B1 B2 = mk_leq R (mk_Times (B1, B2));
  11.143 -    val bis_le = Library.foldr1 HOLogic.mk_conj (map3 mk_bis_le_conjunct Rs Bs B's)
  11.144 +    val bis_le = Library.foldr1 HOLogic.mk_conj (@{map 3} mk_bis_le_conjunct Rs Bs B's)
  11.145  
  11.146      val bis_spec =
  11.147        let
  11.148 @@ -519,7 +520,7 @@
  11.149  
  11.150          val rhs = HOLogic.mk_conj
  11.151            (bis_le, Library.foldr1 HOLogic.mk_conj
  11.152 -            (map9 mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss))
  11.153 +            (@{map 9} mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss))
  11.154        in
  11.155          fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ Rs) rhs
  11.156        end;
  11.157 @@ -563,7 +564,7 @@
  11.158  
  11.159          val rhs = HOLogic.mk_conj
  11.160            (bis_le, Library.foldr1 HOLogic.mk_conj
  11.161 -            (map6 mk_conjunct Rs ss s's zs z's relsAsBs))
  11.162 +            (@{map 6} mk_conjunct Rs ss s's zs z's relsAsBs))
  11.163        in
  11.164          Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs))
  11.165            (K (mk_bis_rel_tac m bis_def in_rels map_comps map_cong0s set_mapss))
  11.166 @@ -684,7 +685,7 @@
  11.167          fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis Bs ss i));
  11.168          val goals = map2 (fn i => fn R => Logic.mk_implies (sbis_prem, mk_concl i R)) ks sRs;
  11.169        in
  11.170 -        map3 (fn goal => fn i => fn def =>
  11.171 +        @{map 3} (fn goal => fn i => fn def =>
  11.172            Goal.prove_sorry lthy [] [] goal (K (mk_incl_lsbis_tac n i def))
  11.173            |> Thm.close_derivation
  11.174            |> singleton (Proof_Context.export names_lthy lthy)) goals ks lsbis_defs
  11.175 @@ -695,7 +696,7 @@
  11.176          fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis Bs ss i));
  11.177          val goals = map2 (fn i => fn B => Logic.mk_implies (coalg_prem, mk_concl i B)) ks Bs;
  11.178        in
  11.179 -        map3 (fn goal => fn l_incl => fn incl_l =>
  11.180 +        @{map 3} (fn goal => fn l_incl => fn incl_l =>
  11.181            Goal.prove_sorry lthy [] [] goal
  11.182              (K (mk_equiv_lsbis_tac sbis_lsbis_thm l_incl incl_l
  11.183                bis_Id_on_thm bis_converse_thm bis_O_thm))
  11.184 @@ -755,7 +756,7 @@
  11.185            fun mk_set_sbd i bd_Card_order bds =
  11.186              map (fn thm => @{thm ordLeq_ordIso_trans} OF
  11.187                [bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds;
  11.188 -          val set_sbdss = map3 mk_set_sbd ks bd_Card_orders set_bdss;
  11.189 +          val set_sbdss = @{map 3} mk_set_sbd ks bd_Card_orders set_bdss;
  11.190         in
  11.191           (lthy, sbd, sbdT, sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss)
  11.192         end;
  11.193 @@ -765,7 +766,7 @@
  11.194      val sum_sbd_listT = HOLogic.listT sum_sbdT;
  11.195      val sum_sbd_list_setT = HOLogic.mk_setT sum_sbd_listT;
  11.196      val bdTs = passiveAs @ replicate n sbdT;
  11.197 -    val to_sbd_maps = map4 mk_map_of_bnf Dss Ass (replicate n bdTs) bnfs;
  11.198 +    val to_sbd_maps = @{map 4} mk_map_of_bnf Dss Ass (replicate n bdTs) bnfs;
  11.199      val bdFTs = mk_FTs bdTs;
  11.200      val sbdFT = mk_sumTN bdFTs;
  11.201      val treeT = HOLogic.mk_prodT (sum_sbd_list_setT, sum_sbd_listT --> sbdFT);
  11.202 @@ -773,15 +774,15 @@
  11.203      val treeTs = passiveAs @ replicate n treeT;
  11.204      val treeQTs = passiveAs @ replicate n treeQT;
  11.205      val treeFTs = mk_FTs treeTs;
  11.206 -    val tree_maps = map4 mk_map_of_bnf Dss (replicate n bdTs) (replicate n treeTs) bnfs;
  11.207 -    val final_maps = map4 mk_map_of_bnf Dss (replicate n treeTs) (replicate n treeQTs) bnfs;
  11.208 +    val tree_maps = @{map 4} mk_map_of_bnf Dss (replicate n bdTs) (replicate n treeTs) bnfs;
  11.209 +    val final_maps = @{map 4} mk_map_of_bnf Dss (replicate n treeTs) (replicate n treeQTs) bnfs;
  11.210      val isNode_setss = mk_setss (passiveAs @ replicate n sbdT);
  11.211  
  11.212      val root = HOLogic.mk_set sum_sbd_listT [HOLogic.mk_list sum_sbdT []];
  11.213      val Zero = HOLogic.mk_tuple (map (fn U => absdummy U root) activeAs);
  11.214      val Lev_recT = fastype_of Zero;
  11.215  
  11.216 -    val Nil = HOLogic.mk_tuple (map3 (fn i => fn z => fn z'=>
  11.217 +    val Nil = HOLogic.mk_tuple (@{map 3} (fn i => fn z => fn z'=>
  11.218        Term.absfree z' (mk_InN activeAs z i)) ks zs zs');
  11.219      val rv_recT = fastype_of Nil;
  11.220  
  11.221 @@ -812,7 +813,7 @@
  11.222      val isNodeT =
  11.223        Library.foldr (op -->) (map fastype_of [Kl, lab, kl], HOLogic.boolT);
  11.224  
  11.225 -    val Succs = map3 (fn i => fn k => fn k' =>
  11.226 +    val Succs = @{map 3} (fn i => fn k => fn k' =>
  11.227        HOLogic.mk_Collect (fst k', snd k', HOLogic.mk_mem (mk_InN sbdTs k i, mk_Succ Kl kl)))
  11.228        ks kks kks';
  11.229  
  11.230 @@ -828,7 +829,7 @@
  11.231  
  11.232      val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
  11.233        lthy
  11.234 -      |> fold_map3 (fn i => fn x => fn sets => Local_Theory.define
  11.235 +      |> @{fold_map 3} (fn i => fn x => fn sets => Local_Theory.define
  11.236          ((isNode_bind i, NoSyn), (isNode_def_bind i, isNode_spec sets x i)))
  11.237          ks xs isNode_setss
  11.238        |>> apsnd split_list o split_list
  11.239 @@ -848,7 +849,7 @@
  11.240          val empty = HOLogic.mk_mem (HOLogic.mk_list sum_sbdT [], Kl);
  11.241  
  11.242          val tree = mk_Ball Kl (Term.absfree kl'
  11.243 -          (Library.foldr1 HOLogic.mk_conj (map4 (fn Succ => fn i => fn k => fn k' =>
  11.244 +          (Library.foldr1 HOLogic.mk_conj (@{map 4} (fn Succ => fn i => fn k => fn k' =>
  11.245              mk_Ball Succ (Term.absfree k' (mk_isNode
  11.246                (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i])) i)))
  11.247            Succs ks kks kks')));
  11.248 @@ -889,7 +890,7 @@
  11.249            let val in_k = mk_InN sbdTs k i;
  11.250            in Term.absfree k' (HOLogic.mk_prod (mk_Shift Kl in_k, mk_shift lab in_k)) end;
  11.251  
  11.252 -        val f = Term.list_comb (mapFT, passive_ids @ map3 mk_f ks kks kks');
  11.253 +        val f = Term.list_comb (mapFT, passive_ids @ @{map 3} mk_f ks kks kks');
  11.254          val (fTs1, fTs2) = apsnd tl (chop (i - 1) (map (fn T => T --> FT) bdFTs));
  11.255          val fs = map mk_undefined fTs1 @ (f :: map mk_undefined fTs2);
  11.256        in
  11.257 @@ -899,7 +900,7 @@
  11.258  
  11.259      val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) =
  11.260        lthy
  11.261 -      |> fold_map3 (fn i => fn mapFT => fn FT => Local_Theory.define
  11.262 +      |> @{fold_map 3} (fn i => fn mapFT => fn FT => Local_Theory.define
  11.263          ((strT_bind i, NoSyn), (strT_def_bind i, strT_spec mapFT FT i)))
  11.264          ks tree_maps treeFTs
  11.265        |>> apsnd split_list o split_list
  11.266 @@ -955,11 +956,11 @@
  11.267                    (HOLogic.mk_conj (Cons, HOLogic.mk_conj (b_set, kl_rec))))
  11.268                end;
  11.269            in
  11.270 -            Term.absfree a' (Library.foldl1 mk_union (map3 mk_set ks sets zs_copy))
  11.271 +            Term.absfree a' (Library.foldl1 mk_union (@{map 3} mk_set ks sets zs_copy))
  11.272            end;
  11.273  
  11.274          val Suc = Term.absdummy HOLogic.natT (Term.absfree Lev_rec'
  11.275 -          (HOLogic.mk_tuple (map5 mk_Suc ks ss setssAs zs zs')));
  11.276 +          (HOLogic.mk_tuple (@{map 5} mk_Suc ks ss setssAs zs zs')));
  11.277  
  11.278          val rhs = mk_rec_nat Zero Suc;
  11.279        in
  11.280 @@ -1002,7 +1003,7 @@
  11.281            end;
  11.282  
  11.283          val Cons = Term.absfree sumx' (Term.absdummy sum_sbd_listT (Term.absfree rv_rec'
  11.284 -          (HOLogic.mk_tuple (map4 mk_Cons ks ss zs zs'))));
  11.285 +          (HOLogic.mk_tuple (@{map 4} mk_Cons ks ss zs zs'))));
  11.286  
  11.287          val rhs = mk_rec_list Nil Cons;
  11.288        in
  11.289 @@ -1043,7 +1044,7 @@
  11.290              (Term.list_comb (to_sbd_map, passive_ids @ map (mk_to_sbd s k i) ks) $ (s $ k)) i);
  11.291  
  11.292          val Lab = Term.absfree kl'
  11.293 -          (mk_case_sumN (map5 mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z));
  11.294 +          (mk_case_sumN (@{map 5} mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z));
  11.295  
  11.296          val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
  11.297            (Term.absfree nat' (mk_Lev ss nat i $ z)), Lab);
  11.298 @@ -1053,7 +1054,7 @@
  11.299  
  11.300      val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) =
  11.301        lthy
  11.302 -      |> fold_map2 (fn i => fn z =>
  11.303 +      |> @{fold_map 2} (fn i => fn z =>
  11.304          Local_Theory.define ((beh_bind i, NoSyn), (beh_def_bind i, beh_spec i z))) ks zs
  11.305        |>> apsnd split_list o split_list
  11.306        ||> `Local_Theory.restore;
  11.307 @@ -1141,11 +1142,12 @@
  11.308                        mk_Lev ss (HOLogic.mk_Suc nat) i $ z));
  11.309                in
  11.310                  HOLogic.mk_imp (HOLogic.mk_eq (mk_rv ss kl i $ z, mk_InN activeAs z' i'),
  11.311 -                  (Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct'' ks (drop m sets) zs_copy2)))
  11.312 +                  (Library.foldr1 HOLogic.mk_conj
  11.313 +                    (@{map 3} mk_conjunct'' ks (drop m sets) zs_copy2)))
  11.314                end;
  11.315            in
  11.316              HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z),
  11.317 -              Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct' ks setssAs ss zs_copy))
  11.318 +              Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct' ks setssAs ss zs_copy))
  11.319            end;
  11.320  
  11.321          val goal = list_all_free (kl :: zs @ zs_copy @ zs_copy2)
  11.322 @@ -1180,7 +1182,7 @@
  11.323                  HOLogic.mk_imp (HOLogic.mk_mem
  11.324                    (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i']),
  11.325                      mk_Lev ss (HOLogic.mk_Suc nat) i $ z),
  11.326 -                  (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct'' ks sets ss zs_copy)))
  11.327 +                  (Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct'' ks sets ss zs_copy)))
  11.328                end;
  11.329            in
  11.330              HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z),
  11.331 @@ -1238,9 +1240,9 @@
  11.332            HOLogic.mk_Trueprop (mk_congruent R (HOLogic.mk_comp
  11.333              (Term.list_comb (final_map, passive_ids @ map mk_proj lsbisAs), strT)));
  11.334  
  11.335 -        val goals = map3 mk_goal lsbisAs final_maps strTAs;
  11.336 +        val goals = @{map 3} mk_goal lsbisAs final_maps strTAs;
  11.337        in
  11.338 -        map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 =>
  11.339 +        @{map 4} (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 =>
  11.340            Goal.prove_sorry lthy [] [] goal
  11.341              (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong0 equiv_LSBIS_thms))
  11.342            |> Thm.close_derivation)
  11.343 @@ -1265,7 +1267,7 @@
  11.344  
  11.345      val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
  11.346        lthy
  11.347 -      |> fold_map4 (fn b => fn mx => fn car_final => fn in_car_final =>
  11.348 +      |> @{fold_map 4} (fn b => fn mx => fn car_final => fn in_car_final =>
  11.349          typedef (b, params, mx) car_final NONE
  11.350            (EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms
  11.351        |>> apsnd split_list o split_list;
  11.352 @@ -1323,7 +1325,7 @@
  11.353  
  11.354      val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
  11.355        lthy
  11.356 -      |> fold_map6 (fn i => fn rep => fn str => fn mapx => fn Jz => fn Jz' =>
  11.357 +      |> @{fold_map 6} (fn i => fn rep => fn str => fn mapx => fn Jz => fn Jz' =>
  11.358          Local_Theory.define ((dtor_bind i, NoSyn),
  11.359            (dtor_def_bind i, dtor_spec rep str mapx Jz Jz')))
  11.360          ks Rep_Ts str_finals map_FTs Jzs Jzs'
  11.361 @@ -1368,7 +1370,7 @@
  11.362  
  11.363      val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) =
  11.364        lthy
  11.365 -      |> fold_map4 (fn i => fn abs => fn f => fn z =>
  11.366 +      |> @{fold_map 4} (fn i => fn abs => fn f => fn z =>
  11.367          Local_Theory.define ((unfold_bind i, NoSyn), (unfold_def_bind i, unfold_spec abs f z)))
  11.368            ks Abs_Ts (map (fn i => HOLogic.mk_comp
  11.369              (mk_proj (nth lsbisAs (i - 1)), mk_beh ss i)) ks) zs
  11.370 @@ -1379,7 +1381,7 @@
  11.371      val unfolds = map (Morphism.term phi) unfold_frees;
  11.372      val unfold_names = map (fst o dest_Const) unfolds;
  11.373      fun mk_unfolds passives actives =
  11.374 -      map3 (fn name => fn T => fn active =>
  11.375 +      @{map 3} (fn name => fn T => fn active =>
  11.376          Const (name, Library.foldr (op -->)
  11.377            (map2 (curry op -->) actives (mk_FTs (passives @ actives)), active --> T)))
  11.378        unfold_names (mk_Ts passives) actives;
  11.379 @@ -1478,9 +1480,9 @@
  11.380        let
  11.381          fun mk_goal dtor ctor FT =
  11.382           mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
  11.383 -        val goals = map3 mk_goal dtors ctors FTs;
  11.384 +        val goals = @{map 3} mk_goal dtors ctors FTs;
  11.385        in
  11.386 -        map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L =>
  11.387 +        @{map 5} (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L =>
  11.388            Goal.prove_sorry lthy [] [] goal
  11.389              (fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id
  11.390                map_cong0L unfold_o_dtor_thms)
  11.391 @@ -1521,7 +1523,7 @@
  11.392      val corec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o corec_bind;
  11.393  
  11.394      val corec_strs =
  11.395 -      map3 (fn dtor => fn sum_s => fn mapx =>
  11.396 +      @{map 3} (fn dtor => fn sum_s => fn mapx =>
  11.397          mk_case_sum
  11.398            (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s))
  11.399        dtors corec_ss corec_maps;
  11.400 @@ -1532,7 +1534,7 @@
  11.401  
  11.402      val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) =
  11.403        lthy
  11.404 -      |> fold_map3 (fn i => fn T => fn AT =>
  11.405 +      |> @{fold_map 3} (fn i => fn T => fn AT =>
  11.406          Local_Theory.define ((corec_bind i, NoSyn), (corec_def_bind i, corec_spec i T AT)))
  11.407            ks Ts activeAs
  11.408        |>> apsnd split_list o split_list
  11.409 @@ -1544,7 +1546,7 @@
  11.410      fun mk_corecs Ts passives actives =
  11.411        let val Tactives = map2 (curry mk_sumT) Ts actives;
  11.412        in
  11.413 -        map3 (fn name => fn T => fn active =>
  11.414 +        @{map 3} (fn name => fn T => fn active =>
  11.415            Const (name, Library.foldr (op -->)
  11.416              (map2 (curry op -->) actives (mk_FTs (passives @ Tactives)), active --> T)))
  11.417          corec_names Ts actives
  11.418 @@ -1565,9 +1567,9 @@
  11.419            in
  11.420              mk_Trueprop_eq (lhs, rhs)
  11.421            end;
  11.422 -        val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs;
  11.423 +        val goals = @{map 5} mk_goal ks corec_ss corec_maps_rev dtors zs;
  11.424        in
  11.425 -        map3 (fn goal => fn unfold => fn map_cong0 =>
  11.426 +        @{map 3} (fn goal => fn unfold => fn map_cong0 =>
  11.427            Goal.prove_sorry lthy [] [] goal
  11.428              (fn {context = ctxt, prems = _} => mk_corec_tac ctxt m corec_defs unfold map_cong0
  11.429                corec_Inl_sum_thms)
  11.430 @@ -1611,7 +1613,7 @@
  11.431  
  11.432          fun mk_concl phi z1 z2 = HOLogic.mk_imp (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2));
  11.433          val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  11.434 -          (map3 mk_concl phis Jzs1 Jzs2));
  11.435 +          (@{map 3} mk_concl phis Jzs1 Jzs2));
  11.436  
  11.437          fun mk_rel_prem phi dtor rel Jz Jz_copy =
  11.438            let
  11.439 @@ -1622,7 +1624,7 @@
  11.440                (list_all_free [Jz, Jz_copy] (HOLogic.mk_imp (phi $ Jz $ Jz_copy, concl)))
  11.441            end;
  11.442  
  11.443 -        val rel_prems = map5 mk_rel_prem phis dtors rels Jzs Jzs_copy;
  11.444 +        val rel_prems = @{map 5} mk_rel_prem phis dtors rels Jzs Jzs_copy;
  11.445          val dtor_coinduct_goal = Logic.list_implies (rel_prems, concl);
  11.446  
  11.447          val dtor_coinduct =
  11.448 @@ -1720,14 +1722,14 @@
  11.449                end;
  11.450  
  11.451              val Suc = Term.absdummy HOLogic.natT (Term.absfree hrec'
  11.452 -              (HOLogic.mk_tuple (map4 mk_Suc dtors FTs_setss Jzs Jzs')));
  11.453 +              (HOLogic.mk_tuple (@{map 4} mk_Suc dtors FTs_setss Jzs Jzs')));
  11.454            in
  11.455              mk_rec_nat Zero Suc
  11.456            end;
  11.457  
  11.458          val ((col_frees, (_, col_def_frees)), (lthy, lthy_old)) =
  11.459            lthy
  11.460 -          |> fold_map4 (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define
  11.461 +          |> @{fold_map 4} (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define
  11.462              ((col_bind j, NoSyn), (col_def_bind j, col_spec j Zero hrec hrec')))
  11.463              ls Zeros hrecs hrecs'
  11.464            |>> apsnd split_list o split_list
  11.465 @@ -1758,7 +1760,7 @@
  11.466          val setss = map (fn i => map2 (mk_set Ts i) ls passiveAs) ks;
  11.467  
  11.468          val (Jbnf_consts, lthy) =
  11.469 -          fold_map7 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn T =>
  11.470 +          @{fold_map 7} (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn T =>
  11.471                fn lthy =>
  11.472              define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads)
  11.473                map_b rel_b set_bs
  11.474 @@ -1766,10 +1768,10 @@
  11.475                  [Const (@{const_name undefined}, T)]), NONE) lthy)
  11.476            bs map_bs rel_bs set_bss fs_maps setss Ts lthy;
  11.477  
  11.478 -        val (_, Jconsts, Jconst_defs, mk_Jconsts) = split_list4 Jbnf_consts;
  11.479 -        val (_, Jsetss, Jbds_Ds, _, _) = split_list5 Jconsts;
  11.480 -        val (Jmap_defs, Jset_defss, Jbd_defs, _, Jrel_defs) = split_list5 Jconst_defs;
  11.481 -        val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, _) = split_list5 mk_Jconsts;
  11.482 +        val (_, Jconsts, Jconst_defs, mk_Jconsts) = @{split_list 4} Jbnf_consts;
  11.483 +        val (_, Jsetss, Jbds_Ds, _, _) = @{split_list 5} Jconsts;
  11.484 +        val (Jmap_defs, Jset_defss, Jbd_defs, _, Jrel_defs) = @{split_list 5} Jconst_defs;
  11.485 +        val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, _) = @{split_list 5} mk_Jconsts;
  11.486  
  11.487          val Jrel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Jrel_defs;
  11.488          val Jset_defs = flat Jset_defss;
  11.489 @@ -1793,9 +1795,9 @@
  11.490            let
  11.491              fun mk_goal fs_Jmap map dtor dtor' = mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_Jmap),
  11.492                HOLogic.mk_comp (Term.list_comb (map, fs @ fs_Jmaps), dtor));
  11.493 -            val goals = map4 mk_goal fs_Jmaps map_FTFT's dtors dtor's;
  11.494 +            val goals = @{map 4} mk_goal fs_Jmaps map_FTFT's dtors dtor's;
  11.495              val maps =
  11.496 -              map5 (fn goal => fn unfold => fn map_comp => fn map_cong0 => fn map_arg_cong =>
  11.497 +              @{map 5} (fn goal => fn unfold => fn map_comp => fn map_cong0 => fn map_arg_cong =>
  11.498                  Goal.prove_sorry lthy [] [] goal
  11.499                    (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
  11.500                       mk_map_tac m n map_arg_cong unfold map_comp map_cong0)
  11.501 @@ -1811,7 +1813,7 @@
  11.502              fun mk_prem u map dtor dtor' =
  11.503                mk_Trueprop_eq (HOLogic.mk_comp (dtor', u),
  11.504                  HOLogic.mk_comp (Term.list_comb (map, fs @ us), dtor));
  11.505 -            val prems = map4 mk_prem us map_FTFT's dtors dtor's;
  11.506 +            val prems = @{map 4} mk_prem us map_FTFT's dtors dtor's;
  11.507              val goal =
  11.508                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  11.509                  (map2 (curry HOLogic.mk_eq) us fs_Jmaps));
  11.510 @@ -1826,7 +1828,7 @@
  11.511          val Jmap_comp0_thms =
  11.512            let
  11.513              val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  11.514 -              (map3 (fn fmap => fn gmap => fn fgmap =>
  11.515 +              (@{map 3} (fn fmap => fn gmap => fn fgmap =>
  11.516                   HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap))
  11.517                fs_Jmaps gs_Jmaps fgs_Jmaps))
  11.518            in
  11.519 @@ -1849,17 +1851,17 @@
  11.520                    HOLogic.mk_Trueprop (mk_leq (K2 $ x2) (K1 $ x1))));
  11.521  
  11.522              val premss = map2 (fn j => fn Ks =>
  11.523 -              map4 mk_passive_prem (map (fn xs => nth xs (j - 1)) FTs_setss) dtors Jzs Ks @
  11.524 -                flat (map4 (fn sets => fn s => fn x1 => fn K1 =>
  11.525 -                  map3 (mk_active_prem s x1 K1) (drop m sets) Jzs_copy Ks) FTs_setss dtors Jzs Ks))
  11.526 +              @{map 4} mk_passive_prem (map (fn xs => nth xs (j - 1)) FTs_setss) dtors Jzs Ks @
  11.527 +                flat (@{map 4} (fn sets => fn s => fn x1 => fn K1 =>
  11.528 +                  @{map 3} (mk_active_prem s x1 K1) (drop m sets) Jzs_copy Ks) FTs_setss dtors Jzs Ks))
  11.529                ls Kss;
  11.530  
  11.531              val col_minimal_thms =
  11.532                let
  11.533                  fun mk_conjunct j T i K x = mk_leq (mk_col Ts nat i j T $ x) (K $ x);
  11.534                  fun mk_concl j T Ks = list_all_free Jzs
  11.535 -                  (Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks Jzs));
  11.536 -                val concls = map3 mk_concl ls passiveAs Kss;
  11.537 +                  (Library.foldr1 HOLogic.mk_conj (@{map 3} (mk_conjunct j T) ks Ks Jzs));
  11.538 +                val concls = @{map 3} mk_concl ls passiveAs Kss;
  11.539  
  11.540                  val goals = map2 (fn prems => fn concl =>
  11.541                    Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls
  11.542 @@ -1867,7 +1869,7 @@
  11.543                  val ctss =
  11.544                    map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls;
  11.545                in
  11.546 -                map4 (fn goal => fn cts => fn col_0s => fn col_Sucs =>
  11.547 +                @{map 4} (fn goal => fn cts => fn col_0s => fn col_Sucs =>
  11.548                    Goal.prove_sorry lthy [] [] goal
  11.549                      (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s
  11.550                        col_Sucs)
  11.551 @@ -1877,7 +1879,7 @@
  11.552                end;
  11.553  
  11.554              fun mk_conjunct set K x = mk_leq (set $ x) (K $ x);
  11.555 -            fun mk_concl sets Ks = Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct sets Ks Jzs);
  11.556 +            fun mk_concl sets Ks = Library.foldr1 HOLogic.mk_conj (@{map 3} mk_conjunct sets Ks Jzs);
  11.557              val concls = map2 mk_concl Jsetss_by_range Kss;
  11.558  
  11.559              val goals = map2 (fn prems => fn concl =>
  11.560 @@ -1902,14 +1904,14 @@
  11.561                  HOLogic.mk_Trueprop (mk_leq (Jset1 $ x) (Jset2 $ y)));
  11.562  
  11.563              val set_incl_Jset_goalss =
  11.564 -              map4 (fn dtor => fn x => fn sets => fn Jsets =>
  11.565 +              @{map 4} (fn dtor => fn x => fn sets => fn Jsets =>
  11.566                  map2 (mk_set_incl_Jset dtor x) (take m sets) Jsets)
  11.567                dtors Jzs FTs_setss Jsetss_by_bnf;
  11.568  
  11.569              (*x(k) : F(i)set(m+k) (dtor(i) y(i)) ==> J(k)set(j) x(k) <= J(i)set(j) y(i)*)
  11.570              val set_Jset_incl_Jset_goalsss =
  11.571 -              map4 (fn dtori => fn yi => fn sets => fn Jsetsi =>
  11.572 -                map3 (fn xk => fn set => fn Jsetsk =>
  11.573 +              @{map 4} (fn dtori => fn yi => fn sets => fn Jsetsi =>
  11.574 +                @{map 3} (fn xk => fn set => fn Jsetsk =>
  11.575                    map2 (mk_set_Jset_incl_Jset dtori xk yi set) Jsetsk Jsetsi)
  11.576                  Jzs_copy (drop m sets) Jsetss_by_bnf)
  11.577                dtors Jzs FTs_setss Jsetss_by_bnf;
  11.578 @@ -1952,12 +1954,12 @@
  11.579  
  11.580              val cTs = map (SOME o certifyT lthy) params';
  11.581              fun mk_induct_tinst phis jsets y y' =
  11.582 -              map4 (fn phi => fn jset => fn Jz => fn Jz' =>
  11.583 +              @{map 4} (fn phi => fn jset => fn Jz => fn Jz' =>
  11.584                  SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
  11.585                    HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz))))))
  11.586                phis jsets Jzs Jzs';
  11.587            in
  11.588 -            map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
  11.589 +            @{map 6} (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
  11.590                ((set_minimal
  11.591                  |> Drule.instantiate' cTs (mk_induct_tinst phis jsets y y')
  11.592                  |> unfold_thms lthy incls) OF
  11.593 @@ -1976,7 +1978,7 @@
  11.594                     (map2 (fn X => mk_UNION (X $ (dtor $ z))) act_sets sets)));
  11.595              fun mk_goals eq =
  11.596                map2 (fn i => fn sets =>
  11.597 -                map4 (fn Fsets =>
  11.598 +                @{map 4} (fn Fsets =>
  11.599                    mk_simp_goal eq (nth Fsets (i - 1)) (drop m Fsets) sets)
  11.600                  FTs_setss dtors Jzs sets)
  11.601                ls Jsetss_by_range;
  11.602 @@ -1984,7 +1986,7 @@
  11.603              val le_goals = map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj)
  11.604                (mk_goals (uncurry mk_leq));
  11.605              val set_le_thmss = map split_conj_thm
  11.606 -              (map4 (fn goal => fn Jset_minimal => fn set_Jsets => fn set_Jset_Jsetss =>
  11.607 +              (@{map 4} (fn goal => fn Jset_minimal => fn set_Jsets => fn set_Jset_Jsetss =>
  11.608                  Goal.prove_sorry lthy [] [] goal
  11.609                    (K (mk_set_le_tac n Jset_minimal set_Jsets set_Jset_Jsetss))
  11.610                  |> Thm.close_derivation
  11.611 @@ -1993,7 +1995,7 @@
  11.612  
  11.613              val ge_goalss = map (map HOLogic.mk_Trueprop) (mk_goals (uncurry mk_leq o swap));
  11.614              val set_ge_thmss =
  11.615 -              map3 (map3 (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets =>
  11.616 +              @{map 3} (@{map 3} (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets =>
  11.617                  Goal.prove_sorry lthy [] [] goal
  11.618                    (K (mk_set_ge_tac n set_incl_Jset set_Jset_incl_Jsets))
  11.619                  |> Thm.close_derivation
  11.620 @@ -2017,15 +2019,15 @@
  11.621                HOLogic.mk_eq (mk_image f $ (col $ z), col' $ (map $ z));
  11.622  
  11.623              fun mk_goal f cols cols' = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj
  11.624 -              (map4 (mk_col_natural f) fs_Jmaps Jzs cols cols'));
  11.625 +              (@{map 4} (mk_col_natural f) fs_Jmaps Jzs cols cols'));
  11.626  
  11.627 -            val goals = map3 mk_goal fs colss colss';
  11.628 +            val goals = @{map 3} mk_goal fs colss colss';
  11.629  
  11.630              val ctss =
  11.631                map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals;
  11.632  
  11.633              val thms =
  11.634 -              map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
  11.635 +              @{map 4} (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
  11.636                  Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
  11.637                    (fn {context = ctxt, prems = _} => mk_col_natural_tac ctxt cts rec_0s rec_Sucs
  11.638                      dtor_Jmap_thms set_mapss)
  11.639 @@ -2041,7 +2043,7 @@
  11.640              fun mk_col_bd z col bd = mk_ordLeq (mk_card_of (col $ z)) bd;
  11.641  
  11.642              fun mk_goal bds cols = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj
  11.643 -              (map3 mk_col_bd Jzs cols bds));
  11.644 +              (@{map 3} mk_col_bd Jzs cols bds));
  11.645  
  11.646              val goals = map (mk_goal Jbds) colss;
  11.647  
  11.648 @@ -2049,7 +2051,7 @@
  11.649                (map (mk_goal (replicate n sbd)) colss);
  11.650  
  11.651              val thms =
  11.652 -              map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
  11.653 +              @{map 5} (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
  11.654                  Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
  11.655                    (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN
  11.656                      mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss)
  11.657 @@ -2069,7 +2071,7 @@
  11.658                mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y)));
  11.659  
  11.660              fun mk_prems sets z =
  11.661 -              Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys')
  11.662 +              Library.foldr1 HOLogic.mk_conj (@{map 5} (mk_prem z) sets fs fs_copy ys ys')
  11.663  
  11.664              fun mk_map_cong0 sets z fmap gmap =
  11.665                HOLogic.mk_imp (mk_prems sets z, HOLogic.mk_eq (fmap $ z, gmap $ z));
  11.666 @@ -2086,14 +2088,14 @@
  11.667                |> Term.absfree y'
  11.668                |> certify lthy;
  11.669  
  11.670 -            val cphis = map9 mk_cphi
  11.671 +            val cphis = @{map 9} mk_cphi
  11.672                Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy;
  11.673  
  11.674              val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm;
  11.675  
  11.676              val goal =
  11.677                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  11.678 -                (map4 mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps));
  11.679 +                (@{map 4} mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps));
  11.680  
  11.681              val thm =
  11.682                Goal.prove_sorry lthy [] [] goal
  11.683 @@ -2120,9 +2122,9 @@
  11.684            let
  11.685              fun mk_goal Jz Jz' dtor dtor' Jrelphi relphi =
  11.686                mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz'));
  11.687 -            val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
  11.688 +            val goals = @{map 6} mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
  11.689            in
  11.690 -            map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
  11.691 +            @{map 12} (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
  11.692                fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
  11.693                fn set_map0s => fn dtor_set_incls => fn dtor_set_set_inclss =>
  11.694                Goal.prove_sorry lthy [] [] goal
  11.695 @@ -2139,7 +2141,7 @@
  11.696        val zip_ranTs = passiveABs @ prodTsTs';
  11.697        val allJphis = Jphis @ activeJphis;
  11.698        val zipFTs = mk_FTs zip_ranTs;
  11.699 -      val zipTs = map3 (fn T => fn T' => fn FT => T --> T' --> FT) Ts Ts' zipFTs;
  11.700 +      val zipTs = @{map 3} (fn T => fn T' => fn FT => T --> T' --> FT) Ts Ts' zipFTs;
  11.701        val zip_zTs = mk_Ts passiveABs;
  11.702        val (((zips, (abs, abs')), (zip_zs, zip_zs')), names_lthy) = names_lthy
  11.703          |> mk_Frees "zip" zipTs
  11.704 @@ -2176,17 +2178,17 @@
  11.705                    HOLogic.mk_conj (HOLogic.mk_eq (map $ zipxy, dtor $ x),
  11.706                      HOLogic.mk_eq (map' $ zipxy, dtor' $ y))))))
  11.707              end;
  11.708 -          val helper_prems = map9 mk_helper_prem
  11.709 +          val helper_prems = @{map 9} mk_helper_prem
  11.710              activeJphis in_phis zips Jzs Jz's map_all_fsts map_all_snds dtors dtor's;
  11.711            fun mk_helper_coind_phi fst phi x alt y map zip_unfold =
  11.712              list_exists_free [if fst then y else x] (HOLogic.mk_conj (phi $ x $ y,
  11.713                HOLogic.mk_eq (alt, map $ (zip_unfold $ HOLogic.mk_prod (x, y)))))
  11.714 -          val coind1_phis = map6 (mk_helper_coind_phi true)
  11.715 +          val coind1_phis = @{map 6} (mk_helper_coind_phi true)
  11.716              activeJphis Jzs Jzs_copy Jz's Jmap_fsts zip_unfolds;
  11.717 -          val coind2_phis = map6 (mk_helper_coind_phi false)
  11.718 +          val coind2_phis = @{map 6} (mk_helper_coind_phi false)
  11.719                activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds;
  11.720            fun mk_cts zs z's phis =
  11.721 -            map3 (fn z => fn z' => fn phi =>
  11.722 +            @{map 3} (fn z => fn z' => fn phi =>
  11.723                SOME (certify lthy (fold_rev (Term.absfree o Term.dest_Free) [z', z] phi)))
  11.724              zs z's phis @
  11.725              map (SOME o certify lthy) (splice z's zs);
  11.726 @@ -2197,10 +2199,10 @@
  11.727              HOLogic.mk_imp (coind_phi, HOLogic.mk_eq (alt, z));
  11.728            val helper_coind1_concl =
  11.729              HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  11.730 -              (map3 mk_helper_coind_concl Jzs Jzs_copy coind1_phis));
  11.731 +              (@{map 3} mk_helper_coind_concl Jzs Jzs_copy coind1_phis));
  11.732            val helper_coind2_concl =
  11.733              HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  11.734 -              (map3 mk_helper_coind_concl Jz's Jz's_copy coind2_phis));
  11.735 +              (@{map 3} mk_helper_coind_concl Jz's Jz's_copy coind2_phis));
  11.736  
  11.737            fun mk_helper_coind_thms fst concl cts =
  11.738              Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl))
  11.739 @@ -2220,8 +2222,8 @@
  11.740                   HOLogic.mk_eq (z, zip_unfold $ HOLogic.mk_prod (x, y))),
  11.741                phi $ (fst $ ab) $ (snd $ ab)));
  11.742            val helper_ind_phiss =
  11.743 -            map4 (fn Jphi => fn ab => fn fst => fn snd =>
  11.744 -              map5 (mk_helper_ind_phi Jphi ab fst snd)
  11.745 +            @{map 4} (fn Jphi => fn ab => fn fst => fn snd =>
  11.746 +              @{map 5} (mk_helper_ind_phi Jphi ab fst snd)
  11.747                zip_zs activeJphis Jzs Jz's zip_unfolds)
  11.748              Jphis abs fstABs sndABs;
  11.749            val ctss = map2 (fn ab' => fn phis =>
  11.750 @@ -2234,13 +2236,13 @@
  11.751              mk_Ball (set $ z) (Term.absfree ab' ind_phi);
  11.752  
  11.753            val mk_helper_ind_concls =
  11.754 -            map3 (fn ab' => fn ind_phis => fn zip_sets =>
  11.755 -              map3 (mk_helper_ind_concl ab') zip_zs ind_phis zip_sets)
  11.756 +            @{map 3} (fn ab' => fn ind_phis => fn zip_sets =>
  11.757 +              @{map 3} (mk_helper_ind_concl ab') zip_zs ind_phis zip_sets)
  11.758              abs' helper_ind_phiss zip_setss
  11.759              |> map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj);
  11.760  
  11.761            val helper_ind_thmss = if m = 0 then replicate n [] else
  11.762 -            map4 (fn concl => fn j => fn set_induct => fn cts =>
  11.763 +            @{map 4} (fn concl => fn j => fn set_induct => fn cts =>
  11.764                Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl))
  11.765                  (fn {context = ctxt, prems = _} => mk_rel_coinduct_ind_tac ctxt m ks
  11.766                    dtor_unfold_thms set_mapss j (cterm_instantiate_pos cts set_induct))
  11.767 @@ -2262,7 +2264,7 @@
  11.768            let
  11.769              fun mk_le_Jrel_OO Jrelpsi1 Jrelpsi2 Jrelpsi12 =
  11.770                mk_leq (mk_rel_compp (Jrelpsi1, Jrelpsi2)) Jrelpsi12;
  11.771 -            val goals = map3 mk_le_Jrel_OO Jrelpsi1s Jrelpsi2s Jrelpsi12s;
  11.772 +            val goals = @{map 3} mk_le_Jrel_OO Jrelpsi1s Jrelpsi2s Jrelpsi12s;
  11.773  
  11.774              val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
  11.775            in
  11.776 @@ -2380,9 +2382,9 @@
  11.777                      else @{term True}));
  11.778                in
  11.779                  HOLogic.mk_Trueprop
  11.780 -                  (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits))
  11.781 +                  (Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct sets Jzs dummys wits))
  11.782                end;
  11.783 -            val goals = map5 mk_goal Jsetss_by_range ys ys_copy ys'_copy ls;
  11.784 +            val goals = @{map 5} mk_goal Jsetss_by_range ys ys_copy ys'_copy ls;
  11.785            in
  11.786              map2 (fn goal => fn induct =>
  11.787                Goal.prove_sorry lthy [] [] goal
  11.788 @@ -2432,14 +2434,14 @@
  11.789  
  11.790          val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Jrel_unabs_defs;
  11.791  
  11.792 -        val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
  11.793 +        val tacss = @{map 9} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
  11.794            bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
  11.795  
  11.796          fun wit_tac thms ctxt =
  11.797            mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms;
  11.798  
  11.799          val (Jbnfs, lthy) =
  11.800 -          fold_map6 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms =>
  11.801 +          @{fold_map 6} (fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms =>
  11.802                fn consts =>
  11.803              bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms)
  11.804                (SOME deads) map_b rel_b set_bs consts)
    12.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Oct 08 14:34:30 2014 +0200
    12.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Oct 08 17:09:07 2014 +0200
    12.3 @@ -289,7 +289,7 @@
    12.4              val Type (_, dom_Ts) = domain_type (fastype_of1 (bound_Ts, t));
    12.5              val map' = mk_map (length fs) dom_Ts Us map0;
    12.6              val fs' =
    12.7 -              map_flattened_map_args ctxt s (map3 (massage_map_or_map_arg bound_Ts) Us Ts) fs;
    12.8 +              map_flattened_map_args ctxt s (@{map 3} (massage_map_or_map_arg bound_Ts) Us Ts) fs;
    12.9            in
   12.10              Term.list_comb (map', fs')
   12.11            end
   12.12 @@ -325,7 +325,7 @@
   12.13                  val f'_T = typof f';
   12.14                  val arg_Ts = map typof args;
   12.15                in
   12.16 -                Term.list_comb (f', map3 (massage_call bound_Ts) (binder_types f'_T) arg_Ts args)
   12.17 +                Term.list_comb (f', @{map 3} (massage_call bound_Ts) (binder_types f'_T) arg_Ts args)
   12.18                end
   12.19              | NONE =>
   12.20                (case t of
   12.21 @@ -394,7 +394,7 @@
   12.22  
   12.23          fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels};
   12.24        in
   12.25 -        map3 mk_spec ctrs discs selss
   12.26 +        @{map 3} mk_spec ctrs discs selss
   12.27          handle ListPair.UnequalLengths => not_codatatype ctxt res_T
   12.28        end)
   12.29    | _ => not_codatatype ctxt res_T);
   12.30 @@ -452,7 +452,7 @@
   12.31      val (perm_f_hssss, _) = indexedddd perm_f_Tssss h';
   12.32  
   12.33      val fun_arg_hs =
   12.34 -      flat (map3 flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss);
   12.35 +      flat (@{map 3} flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss);
   12.36  
   12.37      fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs;
   12.38      fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs;
   12.39 @@ -486,7 +486,7 @@
   12.40          corec_thm corec_disc corec_sels =
   12.41        let val nullary = not (can dest_funT (fastype_of ctr)) in
   12.42          {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_io,
   12.43 -         calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
   12.44 +         calls = @{map 3} (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
   12.45           distinct_discss = distinct_discss, collapse = collapse, corec_thm = corec_thm,
   12.46           corec_disc = corec_disc, corec_sels = corec_sels}
   12.47        end;
   12.48 @@ -494,7 +494,7 @@
   12.49      fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, distinct_discsss, collapses, ...}
   12.50          : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms corec_discs corec_selss =
   12.51        let val p_ios = map SOME p_is @ [NONE] in
   12.52 -        map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
   12.53 +        @{map 14} mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
   12.54            distinct_discsss collapses corec_thms corec_discs corec_selss
   12.55        end;
   12.56  
   12.57 @@ -509,7 +509,7 @@
   12.58         ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms corec_discs
   12.59           corec_selss};
   12.60    in
   12.61 -    (map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
   12.62 +    (@{map 5} mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
   12.63       co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
   12.64       co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss, coinduct_attrs_pair,
   12.65       is_some gfp_sugar_thms, lthy)
   12.66 @@ -738,7 +738,7 @@
   12.67  
   12.68      val sequentials = replicate (length fun_names) false;
   12.69    in
   12.70 -    fold_map2 (dissect_coeqn_ctr lthy fun_names sequentials basic_ctr_specss eqn_pos eqn0
   12.71 +    @{fold_map 2} (dissect_coeqn_ctr lthy fun_names sequentials basic_ctr_specss eqn_pos eqn0
   12.72          (SOME (abstract (List.rev fun_args) rhs)))
   12.73        ctr_premss ctr_concls matchedsss
   12.74    end;
   12.75 @@ -909,7 +909,7 @@
   12.76      |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
   12.77      |> map2 currys arg_Tss
   12.78      |> Syntax.check_terms lthy
   12.79 -    |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
   12.80 +    |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
   12.81        bs mxs
   12.82      |> rpair excludess'
   12.83    end;
   12.84 @@ -981,7 +981,7 @@
   12.85      val frees = map (fst #>> Binding.name_of #> Free) fixes;
   12.86      val has_call = exists_subterm (member (op =) frees);
   12.87      val eqns_data =
   12.88 -      fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss)
   12.89 +      @{fold_map 2} (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss)
   12.90          (tag_list 0 (map snd specs)) of_specs_opt []
   12.91        |> flat o fst;
   12.92  
   12.93 @@ -1030,7 +1030,7 @@
   12.94        |> map (flat o snd);
   12.95  
   12.96      val arg_Tss = map (binder_types o snd o fst) fixes;
   12.97 -    val disc_eqnss = map6 mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss
   12.98 +    val disc_eqnss = @{map 6} mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss
   12.99        disc_eqnss';
  12.100      val (defs, excludess') =
  12.101        build_codefs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
  12.102 @@ -1045,7 +1045,7 @@
  12.103        else
  12.104          tac_opt;
  12.105  
  12.106 -    val excludess'' = map3 (fn tac_opt => fn sequential => map (fn (j, goal) =>
  12.107 +    val excludess'' = @{map 3} (fn tac_opt => fn sequential => map (fn (j, goal) =>
  12.108          (j, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation)
  12.109             (exclude_tac tac_opt sequential j), goal))))
  12.110        tac_opts sequentials excludess';
  12.111 @@ -1072,7 +1072,7 @@
  12.112          de_facto_exhaustives disc_eqnss
  12.113        |> list_all_fun_args []
  12.114      val nchotomy_taut_thmss =
  12.115 -      map5 (fn tac_opt => fn {exhaust_discs = res_exhaust_discs, ...} =>
  12.116 +      @{map 5} (fn tac_opt => fn {exhaust_discs = res_exhaust_discs, ...} =>
  12.117            fn {code_rhs_opt, ...} :: _ => fn [] => K []
  12.118              | [goal] => fn true =>
  12.119                let
  12.120 @@ -1121,7 +1121,7 @@
  12.121                  end)
  12.122              de_facto_exhaustives disc_eqnss
  12.123            |> list_all_fun_args ps
  12.124 -          |> map3 (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K []
  12.125 +          |> @{map 3} (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K []
  12.126                | [nchotomy_thm] => fn [goal] =>
  12.127                  [mk_primcorec_exhaust_tac lthy ("" (* for "P" *) :: map (fst o dest_Free) fun_args)
  12.128                     (length disc_eqns) nchotomy_thm
  12.129 @@ -1334,9 +1334,9 @@
  12.130                end)
  12.131            end;
  12.132  
  12.133 -        val disc_alistss = map3 (map oo prove_disc) corec_specs excludessss disc_eqnss;
  12.134 +        val disc_alistss = @{map 3} (map oo prove_disc) corec_specs excludessss disc_eqnss;
  12.135          val disc_alists = map (map snd o flat) disc_alistss;
  12.136 -        val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss excludessss sel_eqnss;
  12.137 +        val sel_alists = @{map 4} (map ooo prove_sel) corec_specs disc_eqnss excludessss sel_eqnss;
  12.138          val disc_thmss = map (map snd o sort_list_duplicates o flat) disc_alistss;
  12.139          val disc_thmsss' = map (map (map (snd o snd))) disc_alistss;
  12.140          val sel_thmss = map (map (fst o snd) o sort_list_duplicates) sel_alists;
  12.141 @@ -1364,17 +1364,18 @@
  12.142                |> single
  12.143              end;
  12.144  
  12.145 -        val disc_iff_thmss = map6 (flat ooo map2 oooo prove_disc_iff) corec_specs exhaust_thmss
  12.146 +        val disc_iff_thmss = @{map 6} (flat ooo map2 oooo prove_disc_iff) corec_specs exhaust_thmss
  12.147            disc_thmsss' disc_eqnss disc_thmsss' disc_eqnss
  12.148            |> map sort_list_duplicates;
  12.149  
  12.150 -        val ctr_alists = map6 (fn disc_alist => maps oooo prove_ctr disc_alist) disc_alists
  12.151 +        val ctr_alists = @{map 6} (fn disc_alist => maps oooo prove_ctr disc_alist) disc_alists
  12.152            (map (map snd) sel_alists) corec_specs disc_eqnss sel_eqnss ctr_specss;
  12.153          val ctr_thmss' = map (map snd) ctr_alists;
  12.154          val ctr_thmss = map (map snd o order_list) ctr_alists;
  12.155  
  12.156 -        val code_thmss = map6 prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_thmss'
  12.157 -          ctr_specss;
  12.158 +        val code_thmss =
  12.159 +          @{map 6} prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_thmss'
  12.160 +            ctr_specss;
  12.161  
  12.162          val disc_iff_or_disc_thmss =
  12.163            map2 (fn [] => I | disc_iffs => K disc_iffs) disc_iff_thmss disc_thmss;
    13.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Wed Oct 08 14:34:30 2014 +0200
    13.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Wed Oct 08 17:09:07 2014 +0200
    13.3 @@ -608,7 +608,7 @@
    13.4          else (rtac (sum_case_cong_weak RS trans) THEN'
    13.5            rtac (mk_sum_caseN n i) THEN' rtac (mk_sum_caseN n i RS trans)),
    13.6          rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
    13.7 -        EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
    13.8 +        EVERY' (@{map 3} (fn i' => fn to_sbd_inj => fn from_to_sbd =>
    13.9            DETERM o EVERY' [rtac trans, rtac o_apply, rtac prod_injectI, rtac conjI,
   13.10              rtac trans, rtac @{thm Shift_def},
   13.11              rtac equalityI, rtac subsetI, etac thin_rl,
   13.12 @@ -783,7 +783,7 @@
   13.13    EVERY' [rtac Jset_minimal,
   13.14      REPEAT_DETERM_N n o rtac @{thm Un_upper1},
   13.15      REPEAT_DETERM_N n o
   13.16 -      EVERY' (map3 (fn i => fn set_Jset => fn set_Jset_Jsets =>
   13.17 +      EVERY' (@{map 3} (fn i => fn set_Jset => fn set_Jset_Jsets =>
   13.18          EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnIN n i), etac @{thm UN_I},
   13.19            etac UnE, etac set_Jset, REPEAT_DETERM_N (n - 1) o etac UnE,
   13.20            EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_Jset_Jsets)])
   13.21 @@ -1018,7 +1018,7 @@
   13.22      val snd_diag_nth = if fst then @{thm snd_diag_fst} else @{thm snd_diag_snd};
   13.23    in
   13.24      EVERY' [rtac coinduct,
   13.25 -      EVERY' (map8 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s =>
   13.26 +      EVERY' (@{map 8} (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s =>
   13.27            fn dtor_unfold => fn dtor_map => fn in_rel =>
   13.28          EVERY' [REPEAT_DETERM o resolve_tac [allI, impI, in_rel RS iffD2],
   13.29            REPEAT_DETERM o eresolve_tac [exE, conjE],
   13.30 @@ -1050,7 +1050,7 @@
   13.31    let val n = length ks;
   13.32    in
   13.33      rtac set_induct 1 THEN
   13.34 -    EVERY' (map3 (fn unfold => fn set_map0s => fn i =>
   13.35 +    EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
   13.36        EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
   13.37          select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
   13.38          REPEAT_DETERM o eresolve_tac [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp],
   13.39 @@ -1058,7 +1058,7 @@
   13.40          SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)),
   13.41          rtac subset_refl])
   13.42      unfolds set_map0ss ks) 1 THEN
   13.43 -    EVERY' (map3 (fn unfold => fn set_map0s => fn i =>
   13.44 +    EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
   13.45        EVERY' (map (fn set_map0 =>
   13.46          EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
   13.47          select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
    14.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Oct 08 14:34:30 2014 +0200
    14.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Oct 08 17:09:07 2014 +0200
    14.3 @@ -100,18 +100,18 @@
    14.4      val prod_sTs = map2 (curry op -->) prodFTs activeAs;
    14.5  
    14.6      (* terms *)
    14.7 -    val mapsAsAs = map4 mk_map_of_bnf Dss Ass Ass bnfs;
    14.8 -    val mapsAsBs = map4 mk_map_of_bnf Dss Ass Bss bnfs;
    14.9 -    val mapsBsCs' = map4 mk_map_of_bnf Dss Bss Css' bnfs;
   14.10 -    val mapsAsCs' = map4 mk_map_of_bnf Dss Ass Css' bnfs;
   14.11 -    val map_fsts = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ prodBsAs)) Bss bnfs;
   14.12 -    val map_fsts_rev = map4 mk_map_of_bnf Dss Bss (replicate n (passiveAs @ prodBsAs)) bnfs;
   14.13 -    fun mk_setss Ts = map3 mk_sets_of_bnf (map (replicate live) Dss)
   14.14 +    val mapsAsAs = @{map 4} mk_map_of_bnf Dss Ass Ass bnfs;
   14.15 +    val mapsAsBs = @{map 4} mk_map_of_bnf Dss Ass Bss bnfs;
   14.16 +    val mapsBsCs' = @{map 4} mk_map_of_bnf Dss Bss Css' bnfs;
   14.17 +    val mapsAsCs' = @{map 4} mk_map_of_bnf Dss Ass Css' bnfs;
   14.18 +    val map_fsts = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ prodBsAs)) Bss bnfs;
   14.19 +    val map_fsts_rev = @{map 4} mk_map_of_bnf Dss Bss (replicate n (passiveAs @ prodBsAs)) bnfs;
   14.20 +    fun mk_setss Ts = @{map 3} mk_sets_of_bnf (map (replicate live) Dss)
   14.21        (map (replicate live) (replicate n Ts)) bnfs;
   14.22      val setssAs = mk_setss allAs;
   14.23 -    val bd0s = map3 mk_bd_of_bnf Dss Ass bnfs;
   14.24 +    val bd0s = @{map 3} mk_bd_of_bnf Dss Ass bnfs;
   14.25      val bds =
   14.26 -      map3 (fn bd0 => fn Ds => fn bnf => mk_csum bd0
   14.27 +      @{map 3} (fn bd0 => fn Ds => fn bnf => mk_csum bd0
   14.28          (mk_card_of (HOLogic.mk_UNIV
   14.29            (mk_T_of_bnf Ds (replicate live (fst (dest_relT (fastype_of bd0)))) bnf))))
   14.30        bd0s Dss bnfs;
   14.31 @@ -209,7 +209,7 @@
   14.32          |> singleton (Proof_Context.export names_lthy lthy)
   14.33        end;
   14.34  
   14.35 -    val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
   14.36 +    val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
   14.37  
   14.38      (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>
   14.39        map id ... id f(m+1) ... f(m+n) x = x*)
   14.40 @@ -217,7 +217,7 @@
   14.41        let
   14.42          fun mk_prem set f z z' = HOLogic.mk_Trueprop
   14.43            (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
   14.44 -        val prems = map4 mk_prem (drop m sets) self_fs zs zs';
   14.45 +        val prems = @{map 4} mk_prem (drop m sets) self_fs zs zs';
   14.46          val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
   14.47        in
   14.48          Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
   14.49 @@ -226,7 +226,7 @@
   14.50          |> singleton (Proof_Context.export names_lthy lthy)
   14.51        end;
   14.52  
   14.53 -    val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
   14.54 +    val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
   14.55      val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs;
   14.56      val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs;
   14.57  
   14.58 @@ -240,11 +240,11 @@
   14.59      (*forall i = 1 ... n: (\<forall>x \<in> Fi_in UNIV .. UNIV B1 ... Bn. si x \<in> Bi)*)
   14.60      val alg_spec =
   14.61        let
   14.62 -        val ins = map3 mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs;
   14.63 +        val ins = @{map 3} mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs;
   14.64          fun mk_alg_conjunct B s X x x' =
   14.65            mk_Ball X (Term.absfree x' (HOLogic.mk_mem (s $ x, B)));
   14.66  
   14.67 -        val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_alg_conjunct Bs ss ins xFs xFs')
   14.68 +        val rhs = Library.foldr1 HOLogic.mk_conj (@{map 5} mk_alg_conjunct Bs ss ins xFs xFs')
   14.69        in
   14.70          fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs
   14.71        end;
   14.72 @@ -273,7 +273,7 @@
   14.73          fun mk_prem x set B = HOLogic.mk_Trueprop (mk_leq (set $ x) B);
   14.74          fun mk_concl s x B = mk_Trueprop_mem (s $ x, B);
   14.75          val premss = map2 ((fn x => fn sets => map2 (mk_prem x) (drop m sets) Bs)) xFs setssAs;
   14.76 -        val concls = map3 mk_concl ss xFs Bs;
   14.77 +        val concls = @{map 3} mk_concl ss xFs Bs;
   14.78          val goals = map2 (fn prems => fn concl =>
   14.79            Logic.list_implies (alg_prem :: prems, concl)) premss concls;
   14.80        in
   14.81 @@ -321,9 +321,9 @@
   14.82              (Term.absfree x' (HOLogic.mk_eq (f $ (s $ x), s' $
   14.83                (Term.list_comb (mapAsBs, passive_ids @ fs) $ x))));
   14.84          val rhs = HOLogic.mk_conj
   14.85 -          (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'),
   14.86 +          (Library.foldr1 HOLogic.mk_conj (@{map 5} mk_fbetw fs Bs B's zs zs'),
   14.87            Library.foldr1 HOLogic.mk_conj
   14.88 -            (map8 mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs'))
   14.89 +            (@{map 8} mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs'))
   14.90        in
   14.91          fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs
   14.92        end;
   14.93 @@ -354,7 +354,7 @@
   14.94          fun mk_elim_goal sets mapAsBs f s s' x T =
   14.95            Logic.list_implies ([prem, mk_elim_prem sets x T],
   14.96              mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x])));
   14.97 -        val elim_goals = map7 mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs;
   14.98 +        val elim_goals = @{map 7} mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs;
   14.99          fun prove goal = Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def))
  14.100            |> Thm.close_derivation
  14.101            |> singleton (Proof_Context.export names_lthy lthy);
  14.102 @@ -414,7 +414,7 @@
  14.103  
  14.104      val mor_convol_thm =
  14.105        let
  14.106 -        val maps = map3 (fn s => fn prod_s => fn mapx =>
  14.107 +        val maps = @{map 3} (fn s => fn prod_s => fn mapx =>
  14.108            mk_convol (HOLogic.mk_comp (s, Term.list_comb (mapx, passive_ids @ fsts)), prod_s))
  14.109            s's prod_ss map_fsts;
  14.110        in
  14.111 @@ -432,7 +432,7 @@
  14.112              (HOLogic.mk_comp (f, s),
  14.113              HOLogic.mk_comp (s', Term.list_comb (mapAsBs, passive_ids @ fs)));
  14.114          val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
  14.115 -        val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
  14.116 +        val rhs = Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct mapsAsBs fs ss s's);
  14.117        in
  14.118          Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
  14.119            (K (mk_mor_UNIV_tac m morE_thms mor_def))
  14.120 @@ -490,13 +490,13 @@
  14.121            fun mk_set_sbd i bd_Card_order bds =
  14.122              map (fn thm => @{thm ordLeq_ordIso_trans} OF
  14.123                [bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds;
  14.124 -          val set_sbdss = map3 mk_set_sbd ks bd_Card_orders set_bdss;
  14.125 +          val set_sbdss = @{map 3} mk_set_sbd ks bd_Card_orders set_bdss;
  14.126  
  14.127            fun mk_in_bd_sum i Co Cnz bd =
  14.128              Cnz RS ((@{thm ordLeq_ordIso_trans} OF
  14.129                [Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl}), sbd_ordIso]) RS
  14.130                (bd RS @{thm ordLeq_transitive[OF _ cexp_mono2_Cnotzero[OF _ Card_order_csum]]}));
  14.131 -          val in_sbds = map4 mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds;
  14.132 +          val in_sbds = @{map 4} mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds;
  14.133         in
  14.134           (lthy, sbd, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds)
  14.135         end;
  14.136 @@ -573,7 +573,7 @@
  14.137            Library.foldr1 HOLogic.mk_prodT (map HOLogic.mk_setT BTs));
  14.138        in
  14.139           mk_worec suc_bd (Term.absfree Asi' (Term.absfree idx' (HOLogic.mk_tuple
  14.140 -           (map4 (mk_minH_component Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks))))
  14.141 +           (@{map 4} (mk_minH_component Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks))))
  14.142        end;
  14.143  
  14.144      val (min_algs_thms, min_algs_mono_thms, card_of_min_algs_thm, least_min_algs_thm) =
  14.145 @@ -585,7 +585,7 @@
  14.146  
  14.147          val concl = HOLogic.mk_Trueprop
  14.148            (HOLogic.mk_eq (min_algs $ idx, HOLogic.mk_tuple
  14.149 -            (map4 (mk_minH_component min_algs idx) setssAs FTsAs ss ks)));
  14.150 +            (@{map 4} (mk_minH_component min_algs idx) setssAs FTsAs ss ks)));
  14.151          val goal = Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl);
  14.152  
  14.153          val min_algs_thm = Goal.prove_sorry lthy [] [] goal
  14.154 @@ -696,7 +696,7 @@
  14.155            |> Thm.close_derivation
  14.156            |> singleton (Proof_Context.export names_lthy lthy);
  14.157  
  14.158 -        val leasts = map3 mk_least_thm min_algs Bs min_alg_defs;
  14.159 +        val leasts = @{map 3} mk_least_thm min_algs Bs min_alg_defs;
  14.160  
  14.161          val incl_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
  14.162          val incl = Goal.prove_sorry lthy [] []
  14.163 @@ -811,7 +811,7 @@
  14.164            mk_mor car_inits str_inits Bs ss init_fs_copy];
  14.165          fun mk_fun_eq f g x = HOLogic.mk_eq (f $ x, g $ x);
  14.166          val unique = HOLogic.mk_Trueprop
  14.167 -          (Library.foldr1 HOLogic.mk_conj (map3 mk_fun_eq init_fs init_fs_copy init_xs));
  14.168 +          (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_fun_eq init_fs init_fs_copy init_xs));
  14.169          val cts = map (certify lthy) ss;
  14.170          val unique_mor =
  14.171            Goal.prove_sorry lthy [] [] (Logic.list_implies (prems @ mor_prems, unique))
  14.172 @@ -839,7 +839,7 @@
  14.173            end;
  14.174        in
  14.175          Library.foldr1 HOLogic.mk_conj
  14.176 -          (map6 mk_conjunct phis str_inits active_init_setss init_ins init_xFs init_xFs')
  14.177 +          (@{map 6} mk_conjunct phis str_inits active_init_setss init_ins init_xFs init_xFs')
  14.178        end;
  14.179  
  14.180      val init_induct_thm =
  14.181 @@ -858,7 +858,7 @@
  14.182  
  14.183      val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
  14.184        lthy
  14.185 -      |> fold_map3 (fn b => fn mx => fn car_init =>
  14.186 +      |> @{fold_map 3} (fn b => fn mx => fn car_init =>
  14.187          typedef (b, params, mx) car_init NONE
  14.188            (EVERY' [rtac iffD2, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
  14.189              rtac alg_init_thm] 1)) bs mixfixes car_inits
  14.190 @@ -918,7 +918,7 @@
  14.191  
  14.192      val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
  14.193        lthy
  14.194 -      |> fold_map4 (fn i => fn abs => fn str => fn mapx =>
  14.195 +      |> @{fold_map 4} (fn i => fn abs => fn str => fn mapx =>
  14.196          Local_Theory.define
  14.197            ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec abs str mapx)))
  14.198            ks Abs_Ts str_inits map_FT_inits
  14.199 @@ -945,7 +945,7 @@
  14.200            |> Thm.close_derivation;
  14.201  
  14.202          fun mk_ct initFT str abs = Term.absdummy initFT (abs $ (str $ Bound 0))
  14.203 -        val cts = map3 (certify lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
  14.204 +        val cts = @{map 3} (certify lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
  14.205  
  14.206          val mor_Abs =
  14.207            Goal.prove_sorry lthy [] []
  14.208 @@ -979,7 +979,7 @@
  14.209      val folds = map (Morphism.term phi) fold_frees;
  14.210      val fold_names = map (fst o dest_Const) folds;
  14.211      fun mk_folds passives actives =
  14.212 -      map3 (fn name => fn T => fn active =>
  14.213 +      @{map 3} (fn name => fn T => fn active =>
  14.214          Const (name, Library.foldr (op -->)
  14.215            (map2 (curry op -->) (mk_FTs (passives @ actives)) actives, T --> active)))
  14.216        fold_names (mk_Ts passives) actives;
  14.217 @@ -993,7 +993,7 @@
  14.218      val copy_thm =
  14.219        let
  14.220          val prems = HOLogic.mk_Trueprop (mk_alg Bs ss) ::
  14.221 -          map3 (HOLogic.mk_Trueprop ooo mk_bij_betw) inv_fs B's Bs;
  14.222 +          @{map 3} (HOLogic.mk_Trueprop ooo mk_bij_betw) inv_fs B's Bs;
  14.223          val concl = HOLogic.mk_Trueprop (list_exists_free s's
  14.224            (HOLogic.mk_conj (mk_alg B's s's, mk_mor B's s's Bs ss inv_fs)));
  14.225        in
  14.226 @@ -1094,9 +1094,9 @@
  14.227        let
  14.228          fun mk_goal dtor ctor FT =
  14.229            mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
  14.230 -        val goals = map3 mk_goal dtors ctors FTs;
  14.231 +        val goals = @{map 3} mk_goal dtors ctors FTs;
  14.232        in
  14.233 -        map5 (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_cong0L =>
  14.234 +        @{map 5} (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_cong0L =>
  14.235            Goal.prove_sorry lthy [] [] goal
  14.236              (K (mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_fold_thms))
  14.237            |> Thm.close_derivation)
  14.238 @@ -1136,7 +1136,7 @@
  14.239      val rec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o rec_bind;
  14.240  
  14.241      val rec_strs =
  14.242 -      map3 (fn ctor => fn prod_s => fn mapx =>
  14.243 +      @{map 3} (fn ctor => fn prod_s => fn mapx =>
  14.244          mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s))
  14.245        ctors rec_ss rec_maps;
  14.246  
  14.247 @@ -1146,7 +1146,7 @@
  14.248  
  14.249      val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) =
  14.250        lthy
  14.251 -      |> fold_map3 (fn i => fn T => fn AT =>
  14.252 +      |> @{fold_map 3} (fn i => fn T => fn AT =>
  14.253          Local_Theory.define ((rec_bind i, NoSyn), (rec_def_bind i, rec_spec i T AT))) ks Ts activeAs
  14.254        |>> apsnd split_list o split_list
  14.255        ||> `Local_Theory.restore;
  14.256 @@ -1157,7 +1157,7 @@
  14.257      fun mk_recs Ts passives actives =
  14.258        let val Tactives = map2 (curry HOLogic.mk_prodT) Ts actives;
  14.259        in
  14.260 -        map3 (fn name => fn T => fn active =>
  14.261 +        @{map 3} (fn name => fn T => fn active =>
  14.262            Const (name, Library.foldr (op -->)
  14.263              (map2 (curry op -->) (mk_FTs (passives @ Tactives)) actives, T --> active)))
  14.264          rec_names Ts actives
  14.265 @@ -1177,7 +1177,7 @@
  14.266            in
  14.267              mk_Trueprop_eq (lhs, rhs)
  14.268            end;
  14.269 -        val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs;
  14.270 +        val goals = @{map 5} mk_goal ks rec_ss rec_maps_rev ctors xFs;
  14.271        in
  14.272          map2 (fn goal => fn foldx =>
  14.273            Goal.prove_sorry lthy [] [] goal
  14.274 @@ -1221,13 +1221,13 @@
  14.275                  Logic.all z (Logic.mk_implies (prem, concl))
  14.276                end;
  14.277  
  14.278 -            val IHs = map3 mk_IH phis (drop m sets) Izs;
  14.279 +            val IHs = @{map 3} mk_IH phis (drop m sets) Izs;
  14.280              val concl = HOLogic.mk_Trueprop (phi $ (ctor $ x));
  14.281            in
  14.282              Logic.all x (Logic.list_implies (IHs, concl))
  14.283            end;
  14.284  
  14.285 -        val prems = map4 mk_prem phis ctors FTs_setss xFs;
  14.286 +        val prems = @{map 4} mk_prem phis ctors FTs_setss xFs;
  14.287  
  14.288          fun mk_concl phi z = phi $ z;
  14.289          val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_concl phis Izs));
  14.290 @@ -1261,20 +1261,20 @@
  14.291                  fold_rev Logic.all [z1, z2] (Logic.list_implies ([prem1, prem2], concl))
  14.292                end;
  14.293  
  14.294 -            val IHs = map5 mk_IH phi2s (drop m sets) (drop m sets') Izs1 Izs2;
  14.295 +            val IHs = @{map 5} mk_IH phi2s (drop m sets) (drop m sets') Izs1 Izs2;
  14.296              val concl = HOLogic.mk_Trueprop (phi $ (ctor $ x) $ (ctor' $ y));
  14.297            in
  14.298              fold_rev Logic.all [x, y] (Logic.list_implies (IHs, concl))
  14.299            end;
  14.300  
  14.301 -        val prems = map7 mk_prem phi2s ctors ctor's FTs_setss FTs'_setss xFs yFs;
  14.302 +        val prems = @{map 7} mk_prem phi2s ctors ctor's FTs_setss FTs'_setss xFs yFs;
  14.303  
  14.304          fun mk_concl phi z1 z2 = phi $ z1 $ z2;
  14.305          val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  14.306 -          (map3 mk_concl phi2s Izs1 Izs2));
  14.307 +          (@{map 3} mk_concl phi2s Izs1 Izs2));
  14.308          fun mk_t phi (z1, z1') (z2, z2') =
  14.309            Term.absfree z1' (HOLogic.mk_all (fst z2', snd z2', phi $ z1 $ z2));
  14.310 -        val cts = map3 (SOME o certify lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2');
  14.311 +        val cts = @{map 3} (SOME o certify lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2');
  14.312          val goal = Logic.list_implies (prems, concl);
  14.313        in
  14.314          (Goal.prove_sorry lthy [] [] goal
  14.315 @@ -1347,7 +1347,7 @@
  14.316                  Library.foldl1 mk_union (map mk_UN (drop m sets))))
  14.317            end;
  14.318  
  14.319 -        val colss = map5 (fn l => fn T => map3 (mk_col l T)) ls passiveAs AFss AFss' setsss;
  14.320 +        val colss = @{map 5} (fn l => fn T => @{map 3} (mk_col l T)) ls passiveAs AFss AFss' setsss;
  14.321          val setss_by_range = map (fn cols => map (mk_fold Ts cols) ks) colss;
  14.322          val setss_by_bnf = transpose setss_by_range;
  14.323  
  14.324 @@ -1376,7 +1376,7 @@
  14.325                  |> minimize_wits
  14.326                end;
  14.327            in
  14.328 -            map3 (fn ctor => fn i => map close_wit o minimize_wits o maps (mk_wit witss ctor i))
  14.329 +            @{map 3} (fn ctor => fn i => map close_wit o minimize_wits o maps (mk_wit witss ctor i))
  14.330                ctors (0 upto n - 1) witss
  14.331            end;
  14.332  
  14.333 @@ -1431,23 +1431,23 @@
  14.334                fun mk_set_sbd0 i bd0_Card_order bd0s =
  14.335                  map (fn thm => @{thm ordLeq_ordIso_trans} OF
  14.336                    [bd0_Card_order RS mk_ordLeq_csum n i thm, sbd0_ordIso]) bd0s;
  14.337 -              val set_sbd0ss = map3 mk_set_sbd0 ks bd0_Card_orders set_bd0ss;
  14.338 +              val set_sbd0ss = @{map 3} mk_set_sbd0 ks bd0_Card_orders set_bd0ss;
  14.339              in
  14.340                (lthy, sbd0, sbd0_card_order, sbd0_Cinfinite, set_sbd0ss)
  14.341              end;
  14.342  
  14.343          val (Ibnf_consts, lthy) =
  14.344 -          fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits =>
  14.345 -              fn T => fn lthy =>
  14.346 +          @{fold_map 8} (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
  14.347 +              fn wits => fn T => fn lthy =>
  14.348              define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads)
  14.349                map_b rel_b set_bs
  14.350                ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd0), wits), NONE) lthy)
  14.351            bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy;
  14.352  
  14.353 -        val (_, Iconsts, Iconst_defs, mk_Iconsts) = split_list4 Ibnf_consts;
  14.354 -        val (_, Isetss, Ibds_Ds, Iwitss_Ds, _) = split_list5 Iconsts;
  14.355 -        val (Imap_defs, Iset_defss, Ibd_defs, Iwit_defss, Irel_defs) = split_list5 Iconst_defs;
  14.356 -        val (mk_Imaps_Ds, mk_It_Ds, _, mk_Irels_Ds, _) = split_list5 mk_Iconsts;
  14.357 +        val (_, Iconsts, Iconst_defs, mk_Iconsts) = @{split_list 4} Ibnf_consts;
  14.358 +        val (_, Isetss, Ibds_Ds, Iwitss_Ds, _) = @{split_list 5} Iconsts;
  14.359 +        val (Imap_defs, Iset_defss, Ibd_defs, Iwit_defss, Irel_defs) = @{split_list 5} Iconst_defs;
  14.360 +        val (mk_Imaps_Ds, mk_It_Ds, _, mk_Irels_Ds, _) = @{split_list 5} mk_Iconsts;
  14.361  
  14.362          val Irel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Irel_defs;
  14.363          val Iset_defs = flat Iset_defss;
  14.364 @@ -1474,9 +1474,9 @@
  14.365              fun mk_goal fs_map map ctor ctor' =
  14.366                mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor),
  14.367                  HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_Imaps)));
  14.368 -            val goals = map4 mk_goal fs_Imaps map_FTFT's ctors ctor's;
  14.369 +            val goals = @{map 4} mk_goal fs_Imaps map_FTFT's ctors ctor's;
  14.370              val maps =
  14.371 -              map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong0 =>
  14.372 +              @{map 4} (fn goal => fn foldx => fn map_comp_id => fn map_cong0 =>
  14.373                  Goal.prove_sorry lthy [] [] goal
  14.374                    (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
  14.375                      mk_map_tac m n foldx map_comp_id map_cong0)
  14.376 @@ -1492,7 +1492,7 @@
  14.377              fun mk_prem u map ctor ctor' =
  14.378                mk_Trueprop_eq (HOLogic.mk_comp (u, ctor),
  14.379                  HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ us)));
  14.380 -            val prems = map4 mk_prem us map_FTFT's ctors ctor's;
  14.381 +            val prems = @{map 4} mk_prem us map_FTFT's ctors ctor's;
  14.382              val goal =
  14.383                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  14.384                  (map2 (curry HOLogic.mk_eq) us fs_Imaps));
  14.385 @@ -1513,7 +1513,8 @@
  14.386                mk_Trueprop_eq (HOLogic.mk_comp (set, ctor),
  14.387                  HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets)));
  14.388              val goalss =
  14.389 -              map3 (fn sets => map4 (mk_goal sets) ctors sets) Isetss_by_range colss map_setss;
  14.390 +              @{map 3} (fn sets => @{map 4} (mk_goal sets) ctors sets)
  14.391 +                Isetss_by_range colss map_setss;
  14.392              val setss = map (map2 (fn foldx => fn goal =>
  14.393                  Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
  14.394                    unfold_thms_tac ctxt Iset_defs THEN mk_set_tac foldx)
  14.395 @@ -1526,11 +1527,11 @@
  14.396                    Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets)));
  14.397              val simp_goalss =
  14.398                map2 (fn i => fn sets =>
  14.399 -                map4 (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets)
  14.400 +                @{map 4} (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets)
  14.401                    FTs_setss ctors xFs sets)
  14.402                  ls Isetss_by_range;
  14.403  
  14.404 -            val ctor_setss = map3 (fn i => map3 (fn set_nats => fn goal => fn set =>
  14.405 +            val ctor_setss = @{map 3} (fn i => @{map 3} (fn set_nats => fn goal => fn set =>
  14.406                  Goal.prove_sorry lthy [] [] goal
  14.407                    (K (mk_ctor_set_tac set (nth set_nats (i - 1)) (drop m set_nats)))
  14.408                  |> Thm.close_derivation
  14.409 @@ -1563,21 +1564,21 @@
  14.410  
  14.411              val csetss = map (map (certify lthy)) Isetss_by_range';
  14.412  
  14.413 -            val cphiss = map3 (fn f => fn sets => fn sets' =>
  14.414 -              (map4 (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range';
  14.415 +            val cphiss = @{map 3} (fn f => fn sets => fn sets' =>
  14.416 +              (@{map 4} (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range';
  14.417  
  14.418              val inducts = map (fn cphis =>
  14.419                Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
  14.420  
  14.421              val goals =
  14.422 -              map3 (fn f => fn sets => fn sets' =>
  14.423 +              @{map 3} (fn f => fn sets => fn sets' =>
  14.424                  HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  14.425 -                  (map4 (mk_set_map0 f) fs_Imaps Izs sets sets')))
  14.426 +                  (@{map 4} (mk_set_map0 f) fs_Imaps Izs sets sets')))
  14.427                    fs Isetss_by_range Isetss_by_range';
  14.428  
  14.429              fun mk_tac ctxt induct = mk_set_nat_tac ctxt m (rtac induct) set_mapss ctor_Imap_thms;
  14.430              val thms =
  14.431 -              map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
  14.432 +              @{map 5} (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
  14.433                  Goal.prove_sorry lthy [] [] goal
  14.434                    (fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i)
  14.435                  |> Thm.close_derivation
  14.436 @@ -1601,11 +1602,11 @@
  14.437              val goals =
  14.438                map (fn sets =>
  14.439                  HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  14.440 -                  (map3 mk_set_bd Izs Ibds sets))) Isetss_by_range;
  14.441 +                  (@{map 3} mk_set_bd Izs Ibds sets))) Isetss_by_range;
  14.442  
  14.443              fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac induct) sbd0_Cinfinite set_sbd0ss;
  14.444              val thms =
  14.445 -              map4 (fn goal => fn ctor_sets => fn induct => fn i =>
  14.446 +              @{map 4} (fn goal => fn ctor_sets => fn induct => fn i =>
  14.447                  Goal.prove_sorry lthy [] [] goal
  14.448                      (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Ibd_defs THEN
  14.449                        mk_tac ctxt induct ctor_sets i)
  14.450 @@ -1623,19 +1624,19 @@
  14.451  
  14.452              fun mk_map_cong0 sets z fmap gmap =
  14.453                HOLogic.mk_imp
  14.454 -                (Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys'),
  14.455 +                (Library.foldr1 HOLogic.mk_conj (@{map 5} (mk_prem z) sets fs fs_copy ys ys'),
  14.456                  HOLogic.mk_eq (fmap $ z, gmap $ z));
  14.457  
  14.458              fun mk_cphi sets z fmap gmap =
  14.459                certify lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap));
  14.460  
  14.461 -            val cphis = map4 mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps;
  14.462 +            val cphis = @{map 4} mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps;
  14.463  
  14.464              val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm;
  14.465  
  14.466              val goal =
  14.467                HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
  14.468 -                (map4 mk_map_cong0 Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps));
  14.469 +                (@{map 4} mk_map_cong0 Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps));
  14.470  
  14.471              val thm = Goal.prove_sorry lthy [] [] goal
  14.472                  (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt (rtac induct) set_Iset_thmsss
  14.473 @@ -1666,9 +1667,9 @@
  14.474            let
  14.475              fun mk_goal xF yF ctor ctor' Irelphi relphi =
  14.476                mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF);
  14.477 -            val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
  14.478 +            val goals = @{map 6} mk_goal xFs yFs ctors ctor's Irelphis relphis;
  14.479            in
  14.480 -            map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
  14.481 +            @{map 12} (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
  14.482                fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
  14.483                fn set_map0s => fn ctor_set_incls => fn ctor_set_set_inclss =>
  14.484                Goal.prove_sorry lthy [] [] goal
  14.485 @@ -1686,12 +1687,12 @@
  14.486              fun mk_le_Irel_OO Irelpsi1 Irelpsi2 Irelpsi12 Iz1 Iz2 =
  14.487                HOLogic.mk_imp (mk_rel_compp (Irelpsi1, Irelpsi2) $ Iz1 $ Iz2,
  14.488                  Irelpsi12 $ Iz1 $ Iz2);
  14.489 -            val goals = map5 mk_le_Irel_OO Irelpsi1s Irelpsi2s Irelpsi12s Izs1 Izs2;
  14.490 +            val goals = @{map 5} mk_le_Irel_OO Irelpsi1s Irelpsi2s Irelpsi12s Izs1 Izs2;
  14.491  
  14.492              val cTs = map (SOME o certifyT lthy o TFree) induct2_params;
  14.493              val cxs = map (SOME o certify lthy) (splice Izs1 Izs2);
  14.494              fun mk_cphi z1 z2 goal = SOME (certify lthy (Term.absfree z1 (Term.absfree z2 goal)));
  14.495 -            val cphis = map3 mk_cphi Izs1' Izs2' goals;
  14.496 +            val cphis = @{map 3} mk_cphi Izs1' Izs2' goals;
  14.497              val induct = Drule.instantiate' cTs (cphis @ cxs) ctor_induct2_thm;
  14.498  
  14.499              val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
  14.500 @@ -1720,14 +1721,14 @@
  14.501  
  14.502          val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Irel_unabs_defs;
  14.503  
  14.504 -        val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
  14.505 +        val tacss = @{map 9} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
  14.506            bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
  14.507  
  14.508          fun wit_tac ctxt = unfold_thms_tac ctxt (flat Iwit_defss) THEN
  14.509            mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs);
  14.510  
  14.511          val (Ibnfs, lthy) =
  14.512 -          fold_map5 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts =>
  14.513 +          @{fold_map 5} (fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts =>
  14.514              bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads)
  14.515                map_b rel_b set_bs consts)
  14.516            tacss map_bs rel_bs set_bss
    15.1 --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Oct 08 14:34:30 2014 +0200
    15.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Oct 08 17:09:07 2014 +0200
    15.3 @@ -115,7 +115,7 @@
    15.4      val bs = map mk_binding b_names;
    15.5      val rhss = mk_split_rec_rhs lthy fpTs Cs recs;
    15.6    in
    15.7 -    fold_map3 (define_co_rec_as Least_FP Cs) fpTs bs rhss lthy
    15.8 +    @{fold_map 3} (define_co_rec_as Least_FP Cs) fpTs bs rhss lthy
    15.9    end;
   15.10  
   15.11  fun mk_split_rec_thmss ctxt Xs ctrXs_Tsss ctrss rec0_thmss (recs as rec1 :: _) rec_defs =
   15.12 @@ -149,7 +149,7 @@
   15.13            (mk_Trueprop_eq (frec $ gctr, Term.list_comb (f, fgs)))
   15.14        end;
   15.15  
   15.16 -    val goalss = map4 (map3 o mk_goal) frecs ctrXs_Tsss ctrss fss;
   15.17 +    val goalss = @{map 4} (@{map 3} o mk_goal) frecs ctrXs_Tsss ctrss fss;
   15.18  
   15.19      fun tac ctxt =
   15.20        unfold_thms_tac ctxt (@{thms o_apply fst_conv snd_conv} @ rec_defs @ flat rec0_thmss) THEN
   15.21 @@ -237,7 +237,7 @@
   15.22        (index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs));
   15.23  
   15.24      val fp_ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar o checked_fp_sugar_of) fpT_names;
   15.25 -    val orig_descr = map3 mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars;
   15.26 +    val orig_descr = @{map 3} mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars;
   15.27      val all_infos = Old_Datatype_Data.get_all thy;
   15.28      val (orig_descr' :: nested_descrs) =
   15.29        if member (op =) prefs Keep_Nesting then [orig_descr]
    16.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Oct 08 14:34:30 2014 +0200
    16.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Oct 08 17:09:07 2014 +0200
    16.3 @@ -232,7 +232,7 @@
    16.4        end;
    16.5  
    16.6      fun mk_ctr_specs fp_res_index k ctrs rec_thms =
    16.7 -      map4 mk_ctr_spec ctrs (k upto k + length ctrs - 1) (nth perm_fun_arg_Tssss fp_res_index)
    16.8 +      @{map 4} mk_ctr_spec ctrs (k upto k + length ctrs - 1) (nth perm_fun_arg_Tssss fp_res_index)
    16.9          rec_thms;
   16.10  
   16.11      fun mk_spec ctr_offset
   16.12 @@ -433,7 +433,7 @@
   16.13      (recs, ctr_poss)
   16.14      |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos)
   16.15      |> Syntax.check_terms ctxt
   16.16 -    |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
   16.17 +    |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
   16.18        bs mxs
   16.19    end;
   16.20  
   16.21 @@ -595,11 +595,11 @@
   16.22      val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
   16.23  
   16.24      val mk_notes =
   16.25 -      flat ooo map3 (fn js => fn prefix => fn thms =>
   16.26 +      flat ooo @{map 3} (fn js => fn prefix => fn thms =>
   16.27          let
   16.28            val (bs, attrss) = map_split (fst o nth specs) js;
   16.29            val notes =
   16.30 -            map3 (fn b => fn attrs => fn thm =>
   16.31 +            @{map 3} (fn b => fn attrs => fn thm =>
   16.32                  ((Binding.qualify false prefix b, code_nitpicksimp_simp_attrs @ attrs),
   16.33                   [([thm], [])]))
   16.34                bs attrss thms;
    17.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Wed Oct 08 14:34:30 2014 +0200
    17.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Wed Oct 08 17:09:07 2014 +0200
    17.3 @@ -57,7 +57,7 @@
    17.4        val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs;
    17.5        val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs;
    17.6      in
    17.7 -      (missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
    17.8 +      (missing_arg_Ts, perm0_kks, @{map 3} basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
    17.9         fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, induct_attrs,
   17.10         is_some lfp_sugar_thms, lthy)
   17.11      end;
   17.12 @@ -102,7 +102,7 @@
   17.13            let
   17.14              val Type (_, ran_Ts) = range_type (typof t);
   17.15              val map' = mk_map (length fs) Us ran_Ts map0;
   17.16 -            val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
   17.17 +            val fs' = map_flattened_map_args ctxt s (@{map 3} massage_map_or_map_arg Us Ts) fs;
   17.18            in
   17.19              Term.list_comb (map', fs')
   17.20            end
    18.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Oct 08 14:34:30 2014 +0200
    18.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Oct 08 17:09:07 2014 +0200
    18.3 @@ -192,7 +192,7 @@
    18.4        val nested_size_o_maps = fold (union Thm.eq_thm_prop) nested_size_o_mapss [];
    18.5  
    18.6        val ((raw_size_consts, raw_size_defs), (lthy1', lthy1)) = lthy0
    18.7 -        |> apfst split_list o fold_map2 (fn b => fn rhs =>
    18.8 +        |> apfst split_list o @{fold_map 2} (fn b => fn rhs =>
    18.9              Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
   18.10              #>> apsnd snd)
   18.11            size_bs size_rhss
   18.12 @@ -227,7 +227,7 @@
   18.13        val (overloaded_size_defs, lthy2) = lthy1
   18.14          |> Local_Theory.background_theory_result
   18.15            (Class.instantiation (T_names, map dest_TFree As, [HOLogic.class_size])
   18.16 -           #> fold_map3 define_overloaded_size overloaded_size_def_bs overloaded_size_consts
   18.17 +           #> @{fold_map 3} define_overloaded_size overloaded_size_def_bs overloaded_size_consts
   18.18               overloaded_size_rhss
   18.19             ##> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
   18.20             ##> Local_Theory.exit_global);
   18.21 @@ -324,7 +324,7 @@
   18.22                map2 (fold_rev (fold_rev Logic.all) [gs, hs] o HOLogic.mk_Trueprop oo
   18.23                  curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss;
   18.24              val rec_o_map_thms =
   18.25 -              map3 (fn goal => fn rec_def => fn ctor_rec_o_map =>
   18.26 +              @{map 3} (fn goal => fn rec_def => fn ctor_rec_o_map =>
   18.27                    Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
   18.28                      mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
   18.29                        ctor_rec_o_map)
   18.30 @@ -351,7 +351,7 @@
   18.31  
   18.32              val size_o_map_thmss =
   18.33                if nested_size_o_maps_complete then
   18.34 -                map3 (fn goal => fn size_def => fn rec_o_map =>
   18.35 +                @{map 3} (fn goal => fn size_def => fn rec_o_map =>
   18.36                      Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
   18.37                        mk_size_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps)
   18.38                      |> Thm.close_derivation
    19.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Wed Oct 08 14:34:30 2014 +0200
    19.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Wed Oct 08 17:09:07 2014 +0200
    19.3 @@ -473,7 +473,7 @@
    19.4        EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI,
    19.5          rtac (mor_Abs RS morE RS arg_cong RS iffD2), atac,
    19.6          REPEAT_DETERM o eresolve_tac [CollectE, conjE], dtac @{thm meta_spec},
    19.7 -        EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), atac];
    19.8 +        EVERY' (@{map 3} mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), atac];
    19.9  
   19.10      fun mk_induct_tac (Rep, Rep_inv) =
   19.11        EVERY' [rtac (Rep_inv RS arg_cong RS iffD1), etac (Rep RSN (2, bspec))];
   19.12 @@ -547,7 +547,7 @@
   19.13          REPEAT_DETERM_N (n - 1) o EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]),
   19.14          EVERY' (map useIH (drop m set_nats))];
   19.15    in
   19.16 -    (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1
   19.17 +    (induct_tac THEN' EVERY' (@{map 4} mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1
   19.18    end;
   19.19  
   19.20  fun mk_set_bd_tac ctxt m induct_tac bd_Cinfinite set_bdss ctor_sets i =
   19.21 @@ -581,12 +581,12 @@
   19.22          EVERY' (map useIH (transpose (map tl set_setss))),
   19.23          rtac sym, rtac ctor_map];
   19.24    in
   19.25 -    (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
   19.26 +    (induct_tac THEN' EVERY' (@{map 3} mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
   19.27    end;
   19.28  
   19.29  fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs =
   19.30    EVERY' (rtac induct ::
   19.31 -  map4 (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO =>
   19.32 +  @{map 4} (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO =>
   19.33      EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}),
   19.34        REPEAT_DETERM_N 2 o dtac (Irel RS iffD1), rtac (Irel RS iffD2),
   19.35        rtac rel_mono, rtac (le_rel_OO RS @{thm predicate2D}),
   19.36 @@ -725,7 +725,7 @@
   19.37    in
   19.38      unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
   19.39      EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2,
   19.40 -      EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong0 =>
   19.41 +      EVERY' (@{map 3} (fn IH => fn ctor_rel => fn rel_mono_strong0 =>
   19.42          EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp),
   19.43            etac rel_mono_strong0,
   19.44            REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]},
    20.1 --- a/src/HOL/Tools/BNF/bnf_util.ML	Wed Oct 08 14:34:30 2014 +0200
    20.2 +++ b/src/HOL/Tools/BNF/bnf_util.ML	Wed Oct 08 17:09:07 2014 +0200
    20.3 @@ -10,82 +10,6 @@
    20.4    include CTR_SUGAR_UTIL
    20.5    include BNF_FP_REC_SUGAR_UTIL
    20.6  
    20.7 -  val map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) ->
    20.8 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list
    20.9 -  val map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) ->
   20.10 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list
   20.11 -  val map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i) ->
   20.12 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i list
   20.13 -  val map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j) ->
   20.14 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
   20.15 -    'i list -> 'j list
   20.16 -  val map10: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k) ->
   20.17 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
   20.18 -    'i list -> 'j list -> 'k list
   20.19 -  val map11: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l) ->
   20.20 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
   20.21 -    'i list -> 'j list -> 'k list -> 'l list
   20.22 -  val map12: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm) ->
   20.23 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
   20.24 -    'i list -> 'j list -> 'k list -> 'l list -> 'm list
   20.25 -  val map13: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n) ->
   20.26 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
   20.27 -    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list
   20.28 -  val map14: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
   20.29 -      'o) ->
   20.30 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
   20.31 -    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list
   20.32 -  val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
   20.33 -      'o -> 'p) ->
   20.34 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
   20.35 -    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list
   20.36 -  val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
   20.37 -      'o -> 'p -> 'q) ->
   20.38 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
   20.39 -    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list -> 'q list
   20.40 -  val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) ->
   20.41 -    'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e
   20.42 -  val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) ->
   20.43 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f -> 'g list * 'f
   20.44 -  val fold_map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h * 'g) ->
   20.45 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g -> 'h list * 'g
   20.46 -  val fold_map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i * 'h) ->
   20.47 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h -> 'i list * 'h
   20.48 -  val fold_map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j * 'i) ->
   20.49 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i ->
   20.50 -    'j list * 'i
   20.51 -  val fold_map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k * 'j) ->
   20.52 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
   20.53 -    'i list -> 'j -> 'k list * 'j
   20.54 -  val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
   20.55 -  val split_list5: ('a * 'b * 'c * 'd * 'e) list -> 'a list * 'b list * 'c list * 'd list * 'e list
   20.56 -  val split_list6: ('a * 'b * 'c * 'd * 'e * 'f) list -> 'a list * 'b list * 'c list * 'd list *
   20.57 -    'e list * 'f list
   20.58 -  val split_list7: ('a * 'b * 'c * 'd * 'e * 'f * 'g) list -> 'a list * 'b list * 'c list *
   20.59 -    'd list * 'e list * 'f list * 'g list
   20.60 -  val split_list8: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h) list -> 'a list * 'b list * 'c list *
   20.61 -    'd list * 'e list * 'f list * 'g list * 'h list
   20.62 -  val split_list9: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i) list -> 'a list * 'b list *
   20.63 -    'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list
   20.64 -  val split_list10: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j) list -> 'a list * 'b list *
   20.65 -    'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list
   20.66 -  val split_list11: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k) list -> 'a list *
   20.67 -    'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list *
   20.68 -    'k list
   20.69 -  val split_list12: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l) list -> 'a list *
   20.70 -    'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list *
   20.71 -    'k list * 'l list
   20.72 -  val split_list13: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm) list ->
   20.73 -    'a list * 'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list *
   20.74 -    'j list * 'k list * 'l list * 'm list
   20.75 -  val split_list14: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm * 'n) list ->
   20.76 -    'a list * 'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list *
   20.77 -    'j list * 'k list * 'l list * 'm list * 'n list
   20.78 -  val split_list15:
   20.79 -    ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm * 'n * 'o) list ->
   20.80 -    'a list * 'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list *
   20.81 -    'j list * 'k list * 'l list * 'm list * 'n list * 'o list
   20.82 -
   20.83    val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
   20.84    val mk_Freesss: string -> typ list list list -> Proof.context ->
   20.85      term list list list * Proof.context
   20.86 @@ -192,194 +116,6 @@
   20.87  
   20.88  (* Library proper *)
   20.89  
   20.90 -fun map6 _ [] [] [] [] [] [] = []
   20.91 -  | map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) =
   20.92 -    f x1 x2 x3 x4 x5 x6 :: map6 f x1s x2s x3s x4s x5s x6s
   20.93 -  | map6 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   20.94 -
   20.95 -fun map7 _ [] [] [] [] [] [] [] = []
   20.96 -  | map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) =
   20.97 -    f x1 x2 x3 x4 x5 x6 x7 :: map7 f x1s x2s x3s x4s x5s x6s x7s
   20.98 -  | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   20.99 -
  20.100 -fun map8 _ [] [] [] [] [] [] [] [] = []
  20.101 -  | map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) =
  20.102 -    f x1 x2 x3 x4 x5 x6 x7 x8 :: map8 f x1s x2s x3s x4s x5s x6s x7s x8s
  20.103 -  | map8 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
  20.104 -
  20.105 -fun map9 _ [] [] [] [] [] [] [] [] [] = []
  20.106 -  | map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
  20.107 -      (x9::x9s) =
  20.108 -    f x1 x2 x3 x4 x5 x6 x7 x8 x9 :: map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s
  20.109 -  | map9 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
  20.110 -
  20.111 -fun map10 _ [] [] [] [] [] [] [] [] [] [] = []
  20.112 -  | map10 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
  20.113 -      (x9::x9s) (x10::x10s) =
  20.114 -    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 :: map10 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s
  20.115 -  | map10 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
  20.116 -
  20.117 -fun map11 _ [] [] [] [] [] [] [] [] [] [] [] = []
  20.118 -  | map11 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
  20.119 -      (x9::x9s) (x10::x10s) (x11::x11s) =
  20.120 -    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 :: map11 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s
  20.121 -  | map11 _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
  20.122 -
  20.123 -fun map12 _ [] [] [] [] [] [] [] [] [] [] [] [] = []
  20.124 -  | map12 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
  20.125 -      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) =
  20.126 -    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ::
  20.127 -      map12 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s
  20.128 -  | map12 _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
  20.129 -
  20.130 -fun map13 _ [] [] [] [] [] [] [] [] [] [] [] [] [] = []
  20.131 -  | map13 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
  20.132 -      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) =
  20.133 -    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ::
  20.134 -      map13 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s
  20.135 -  | map13 _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
  20.136 -
  20.137 -fun map14 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
  20.138 -  | map14 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
  20.139 -      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) =
  20.140 -    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ::
  20.141 -      map14 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s
  20.142 -  | map14 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
  20.143 -
  20.144 -fun map15 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
  20.145 -  | map15 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
  20.146 -      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) =
  20.147 -    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ::
  20.148 -      map15 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s
  20.149 -  | map15 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
  20.150 -
  20.151 -fun map16 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
  20.152 -  | map16 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
  20.153 -      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) (x16::x16s) =
  20.154 -    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 ::
  20.155 -      map16 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s x16s
  20.156 -  | map16 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
  20.157 -
  20.158 -fun fold_map4 _ [] [] [] [] acc = ([], acc)
  20.159 -  | fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
  20.160 -    let
  20.161 -      val (x, acc') = f x1 x2 x3 x4 acc;
  20.162 -      val (xs, acc'') = fold_map4 f x1s x2s x3s x4s acc';
  20.163 -    in (x :: xs, acc'') end
  20.164 -  | fold_map4 _ _ _ _ _ _ = raise ListPair.UnequalLengths;
  20.165 -
  20.166 -fun fold_map5 _ [] [] [] [] [] acc = ([], acc)
  20.167 -  | fold_map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) acc =
  20.168 -    let
  20.169 -      val (x, acc') = f x1 x2 x3 x4 x5 acc;
  20.170 -      val (xs, acc'') = fold_map5 f x1s x2s x3s x4s x5s acc';
  20.171 -    in (x :: xs, acc'') end
  20.172 -  | fold_map5 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
  20.173 -
  20.174 -fun fold_map6 _ [] [] [] [] [] [] acc = ([], acc)
  20.175 -  | fold_map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) acc =
  20.176 -    let
  20.177 -      val (x, acc') = f x1 x2 x3 x4 x5 x6 acc;
  20.178 -      val (xs, acc'') = fold_map6 f x1s x2s x3s x4s x5s x6s acc';
  20.179 -    in (x :: xs, acc'') end
  20.180 -  | fold_map6 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
  20.181 -
  20.182 -fun fold_map7 _ [] [] [] [] [] [] [] acc = ([], acc)
  20.183 -  | fold_map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) acc =
  20.184 -    let
  20.185 -      val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 acc;
  20.186 -      val (xs, acc'') = fold_map7 f x1s x2s x3s x4s x5s x6s x7s acc';
  20.187 -    in (x :: xs, acc'') end
  20.188 -  | fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
  20.189 -
  20.190 -fun fold_map8 _ [] [] [] [] [] [] [] [] acc = ([], acc)
  20.191 -  | fold_map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
  20.192 -      acc =
  20.193 -    let
  20.194 -      val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 acc;
  20.195 -      val (xs, acc'') = fold_map8 f x1s x2s x3s x4s x5s x6s x7s x8s acc';
  20.196 -    in (x :: xs, acc'') end
  20.197 -  | fold_map8 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
  20.198 -
  20.199 -fun fold_map9 _ [] [] [] [] [] [] [] [] [] acc = ([], acc)
  20.200 -  | fold_map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
  20.201 -      (x9::x9s) acc =
  20.202 -    let
  20.203 -      val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 x9 acc;
  20.204 -      val (xs, acc'') = fold_map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s acc';
  20.205 -    in (x :: xs, acc'') end
  20.206 -  | fold_map9 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
  20.207 -
  20.208 -fun split_list4 [] = ([], [], [], [])
  20.209 -  | split_list4 ((x1, x2, x3, x4) :: xs) =
  20.210 -    let val (xs1, xs2, xs3, xs4) = split_list4 xs;
  20.211 -    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
  20.212 -
  20.213 -fun split_list5 [] = ([], [], [], [], [])
  20.214 -  | split_list5 ((x1, x2, x3, x4, x5) :: xs) =
  20.215 -    let val (xs1, xs2, xs3, xs4, xs5) = split_list5 xs;
  20.216 -    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5) end;
  20.217 -
  20.218 -fun split_list6 [] = ([], [], [], [], [], [])
  20.219 -  | split_list6 ((x1, x2, x3, x4, x5, x6) :: xs) =
  20.220 -    let val (xs1, xs2, xs3, xs4, xs5, xs6) = split_list6 xs;
  20.221 -    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6) end;
  20.222 -
  20.223 -fun split_list7 [] = ([], [], [], [], [], [], [])
  20.224 -  | split_list7 ((x1, x2, x3, x4, x5, x6, x7) :: xs) =
  20.225 -    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7) = split_list7 xs;
  20.226 -    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7) end;
  20.227 -
  20.228 -fun split_list8 [] = ([], [], [], [], [], [], [], [])
  20.229 -  | split_list8 ((x1, x2, x3, x4, x5, x6, x7, x8) :: xs) =
  20.230 -    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8) = split_list8 xs;
  20.231 -    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8) end;
  20.232 -
  20.233 -fun split_list9 [] = ([], [], [], [], [], [], [], [], [])
  20.234 -  | split_list9 ((x1, x2, x3, x4, x5, x6, x7, x8, x9) :: xs) =
  20.235 -    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9) = split_list9 xs;
  20.236 -    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
  20.237 -        x9 :: xs9) end;
  20.238 -
  20.239 -fun split_list10 [] = ([], [], [], [], [], [], [], [], [], [])
  20.240 -  | split_list10 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) :: xs) =
  20.241 -    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10) = split_list10 xs;
  20.242 -    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
  20.243 -        x9 :: xs9, x10 :: xs10) end;
  20.244 -
  20.245 -fun split_list11 [] = ([], [], [], [], [], [], [], [], [], [], [])
  20.246 -  | split_list11 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) :: xs) =
  20.247 -    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11) = split_list11 xs;
  20.248 -    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
  20.249 -        x9 :: xs9, x10 :: xs10, x11 :: xs11) end;
  20.250 -
  20.251 -fun split_list12 [] = ([], [], [], [], [], [], [], [], [], [], [], [])
  20.252 -  | split_list12 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) :: xs) =
  20.253 -    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12) = split_list12 xs;
  20.254 -    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
  20.255 -        x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12) end;
  20.256 -
  20.257 -fun split_list13 [] = ([], [], [], [], [], [], [], [], [], [], [], [], [])
  20.258 -  | split_list13 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) :: xs) =
  20.259 -    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12, xs13) = split_list13 xs;
  20.260 -    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
  20.261 -        x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12, x13 :: xs13) end;
  20.262 -
  20.263 -fun split_list14 [] = ([], [], [], [], [], [], [], [], [], [], [], [], [], [])
  20.264 -  | split_list14 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) :: xs) =
  20.265 -    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12, xs13, xs14) =
  20.266 -      split_list14 xs;
  20.267 -    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
  20.268 -        x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12, x13 :: xs13, x14 :: xs14) end;
  20.269 -
  20.270 -fun split_list15 [] = ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
  20.271 -  | split_list15 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) :: xs) =
  20.272 -    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12, xs13, xs14, xs15) =
  20.273 -      split_list15 xs;
  20.274 -    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
  20.275 -        x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12, x13 :: xs13, x14 :: xs14, x15 :: xs15)
  20.276 -    end;
  20.277 -
  20.278  val parse_type_arg_constrained =
  20.279    Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
  20.280  
  20.281 @@ -430,8 +166,8 @@
  20.282  
  20.283  val mk_TFreess = fold_map mk_TFrees;
  20.284  
  20.285 -fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss;
  20.286 -fun mk_Freessss x Tssss = fold_map2 mk_Freesss (mk_names (length Tssss) x) Tssss;
  20.287 +fun mk_Freesss x Tsss = @{fold_map 2} mk_Freess (mk_names (length Tsss) x) Tsss;
  20.288 +fun mk_Freessss x Tssss = @{fold_map 2} mk_Freesss (mk_names (length Tssss) x) Tssss;
  20.289  
  20.290  
  20.291  (** Types **)
    21.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Oct 08 14:34:30 2014 +0200
    21.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Oct 08 17:09:07 2014 +0200
    21.3 @@ -414,7 +414,7 @@
    21.4  
    21.5      val disc_bindings =
    21.6        raw_disc_bindings
    21.7 -      |> map4 (fn k => fn m => fn ctr => fn disc =>
    21.8 +      |> @{map 4} (fn k => fn m => fn ctr => fn disc =>
    21.9          qualify false
   21.10            (if Binding.is_empty disc then
   21.11               if m = 0 then equal_binding
   21.12 @@ -428,7 +428,7 @@
   21.13      fun standard_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr;
   21.14  
   21.15      val sel_bindingss =
   21.16 -      map3 (fn ctr => fn m => map2 (fn l => fn sel =>
   21.17 +      @{map 3} (fn ctr => fn m => map2 (fn l => fn sel =>
   21.18          qualify false
   21.19            (if Binding.is_empty sel orelse Binding.eq_name (sel, standard_binding) then
   21.20              standard_sel_binding m l ctr
   21.21 @@ -476,7 +476,7 @@
   21.22  
   21.23      val case_rhs = fold_rev (fold_rev Term.lambda) [fs, [u]]
   21.24        (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $
   21.25 -         Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss)));
   21.26 +         Term.lambda w (Library.foldr1 HOLogic.mk_disj (@{map 3} mk_case_disj xctrs xfs xss)));
   21.27  
   21.28      val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy
   21.29        |> Local_Theory.define ((case_binding, NoSyn),
   21.30 @@ -538,7 +538,7 @@
   21.31              else
   21.32                map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) all_sel_bindings;
   21.33  
   21.34 -          val all_proto_sels = flat (map3 (fn k => fn xs => map (pair k o pair xs)) ks xss xss);
   21.35 +          val all_proto_sels = flat (@{map 3} (fn k => fn xs => map (pair k o pair xs)) ks xss xss);
   21.36            val sel_infos =
   21.37              AList.group (op =) (sel_binding_index ~~ all_proto_sels)
   21.38              |> sort (int_ord o pairself fst)
   21.39 @@ -565,7 +565,7 @@
   21.40              Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
   21.41  
   21.42            fun mk_sel_case_args b proto_sels T =
   21.43 -            map3 (fn Const (c, _) => fn Ts => fn k =>
   21.44 +            @{map 3} (fn Const (c, _) => fn Ts => fn k =>
   21.45                (case AList.lookup (op =) proto_sels k of
   21.46                  NONE =>
   21.47                  (case filter (curry (op =) (c, Binding.name_of b) o fst) sel_defaults of
   21.48 @@ -596,7 +596,7 @@
   21.49  
   21.50            val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
   21.51              lthy
   21.52 -            |> apfst split_list o fold_map3 (fn k => fn exist_xs_u_eq_ctr => fn b =>
   21.53 +            |> apfst split_list o @{fold_map 3} (fn k => fn exist_xs_u_eq_ctr => fn b =>
   21.54                  if Binding.is_empty b then
   21.55                    if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
   21.56                    else pair (alternate_disc k, alternate_disc_no_def)
   21.57 @@ -640,7 +640,7 @@
   21.58              [fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr),
   21.59                Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))];
   21.60        in
   21.61 -        map4 mk_goal xctrs yctrs xss yss
   21.62 +        @{map 4} mk_goal xctrs yctrs xss yss
   21.63        end;
   21.64  
   21.65      val half_distinct_goalss =
   21.66 @@ -686,10 +686,10 @@
   21.67          val case_thms =
   21.68            let
   21.69              val goals =
   21.70 -              map3 (fn xctr => fn xf => fn xs =>
   21.71 +              @{map 3} (fn xctr => fn xf => fn xs =>
   21.72                  fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xctrs xfs xss;
   21.73            in
   21.74 -            map4 (fn k => fn goal => fn injects => fn distinctss =>
   21.75 +            @{map 4} (fn k => fn goal => fn injects => fn distinctss =>
   21.76                  Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
   21.77                    mk_case_tac ctxt n k case_def injects distinctss)
   21.78                  |> Thm.close_derivation)
   21.79 @@ -703,7 +703,7 @@
   21.80                  mk_Trueprop_eq (xf, xg)));
   21.81  
   21.82              val goal =
   21.83 -              Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss xfs xgs,
   21.84 +              Logic.list_implies (uv_eq :: @{map 4} mk_prem xctrs xss xfs xgs,
   21.85                   mk_Trueprop_eq (eta_ufcase, eta_vgcase));
   21.86              val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
   21.87            in
   21.88 @@ -723,10 +723,10 @@
   21.89  
   21.90          fun mk_split_goal xctrs xss xfs =
   21.91            mk_Trueprop_eq (split_lhs, Library.foldr1 HOLogic.mk_conj
   21.92 -            (map3 mk_split_conjunct xctrs xss xfs));
   21.93 +            (@{map 3} mk_split_conjunct xctrs xss xfs));
   21.94          fun mk_split_asm_goal xctrs xss xfs =
   21.95            mk_Trueprop_eq (split_lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj
   21.96 -            (map3 mk_split_disjunct xctrs xss xfs)));
   21.97 +            (@{map 3} mk_split_disjunct xctrs xss xfs)));
   21.98  
   21.99          fun prove_split selss goal =
  21.100            Goal.prove_sorry lthy [] [] goal (fn _ =>
  21.101 @@ -771,7 +771,7 @@
  21.102                  zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
  21.103                      (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
  21.104  
  21.105 -              val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
  21.106 +              val sel_thmss = @{map 3} (map oo make_sel_thm) xss' case_thms sel_defss;
  21.107  
  21.108                fun has_undefined_rhs thm =
  21.109                  (case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of
  21.110 @@ -833,7 +833,7 @@
  21.111                      | mk_thm _ not_discI [distinct] = distinct RS not_discI;
  21.112                    fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss;
  21.113                  in
  21.114 -                  map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
  21.115 +                  @{map 3} mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
  21.116                  end;
  21.117  
  21.118                val nontriv_disc_thmss =
  21.119 @@ -861,7 +861,7 @@
  21.120  
  21.121                    val half_goalss = map mk_goal half_pairss;
  21.122                    val half_thmss =
  21.123 -                    map3 (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
  21.124 +                    @{map 3} (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
  21.125                          fn disc_thm => [prove (mk_half_distinct_disc_tac lthy m discD disc_thm) goal])
  21.126                        half_goalss half_pairss (flat disc_thmss');
  21.127  
  21.128 @@ -893,9 +893,9 @@
  21.129                      in
  21.130                        (prem aconv concl, Logic.all u (Logic.mk_implies (prem, concl)))
  21.131                      end;
  21.132 -                  val (trivs, goals) = map3 mk_goal ms udiscs usel_ctrs |> split_list;
  21.133 +                  val (trivs, goals) = @{map 3} mk_goal ms udiscs usel_ctrs |> split_list;
  21.134                    val thms =
  21.135 -                    map5 (fn m => fn discD => fn sel_thms => fn triv => fn goal =>
  21.136 +                    @{map 5} (fn m => fn discD => fn sel_thms => fn triv => fn goal =>
  21.137                          Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
  21.138                            mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL atac)
  21.139                          |> Thm.close_derivation
  21.140 @@ -933,7 +933,7 @@
  21.141  
  21.142                    val goal =
  21.143                      Library.foldr Logic.list_implies
  21.144 -                      (map5 mk_prems ks udiscs uselss vdiscs vselss, uv_eq);
  21.145 +                      (@{map 5} mk_prems ks udiscs uselss vdiscs vselss, uv_eq);
  21.146                    val uncollapse_thms =
  21.147                      map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss;
  21.148                  in
    22.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Wed Oct 08 14:34:30 2014 +0200
    22.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Wed Oct 08 17:09:07 2014 +0200
    22.3 @@ -100,9 +100,9 @@
    22.4    else
    22.5      let val ks = 1 upto n in
    22.6        HEADGOAL (rtac uexhaust_disc THEN'
    22.7 -        EVERY' (map5 (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse =>
    22.8 +        EVERY' (@{map 5} (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse =>
    22.9            EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac, rtac sym, rtac vexhaust_disc,
   22.10 -            EVERY' (map4 (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse =>
   22.11 +            EVERY' (@{map 4} (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse =>
   22.12                EVERY'
   22.13                  (if k' = k then
   22.14                     [rtac (vuncollapse RS trans), TRY o atac] @
   22.15 @@ -150,7 +150,7 @@
   22.16  
   22.17  fun mk_case_eq_if_tac ctxt n uexhaust cases discss' selss =
   22.18    HEADGOAL (rtac uexhaust THEN'
   22.19 -    EVERY' (map3 (fn casex => fn if_discs => fn sels =>
   22.20 +    EVERY' (@{map 3} (fn casex => fn if_discs => fn sels =>
   22.21          EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)),
   22.22            rtac casex])
   22.23        cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss));
    23.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Wed Oct 08 14:34:30 2014 +0200
    23.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Wed Oct 08 17:09:07 2014 +0200
    23.3 @@ -10,13 +10,6 @@
    23.4  sig
    23.5    val map_prod: ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd
    23.6  
    23.7 -  val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
    23.8 -  val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
    23.9 -  val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) ->
   23.10 -    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list
   23.11 -  val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c
   23.12 -  val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) ->
   23.13 -    'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd
   23.14    val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
   23.15    val transpose: 'a list list -> 'a list list
   23.16    val pad_list: 'a -> int -> 'a list -> 'a list
   23.17 @@ -108,35 +101,6 @@
   23.18  
   23.19  fun map_prod f g (x, y) = (f x, g y);
   23.20  
   23.21 -fun map3 _ [] [] [] = []
   23.22 -  | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s
   23.23 -  | map3 _ _ _ _ = raise ListPair.UnequalLengths;
   23.24 -
   23.25 -fun map4 _ [] [] [] [] = []
   23.26 -  | map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) = f x1 x2 x3 x4 :: map4 f x1s x2s x3s x4s
   23.27 -  | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
   23.28 -
   23.29 -fun map5 _ [] [] [] [] [] = []
   23.30 -  | map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) =
   23.31 -    f x1 x2 x3 x4 x5 :: map5 f x1s x2s x3s x4s x5s
   23.32 -  | map5 _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   23.33 -
   23.34 -fun fold_map2 _ [] [] acc = ([], acc)
   23.35 -  | fold_map2 f (x1::x1s) (x2::x2s) acc =
   23.36 -    let
   23.37 -      val (x, acc') = f x1 x2 acc;
   23.38 -      val (xs, acc'') = fold_map2 f x1s x2s acc';
   23.39 -    in (x :: xs, acc'') end
   23.40 -  | fold_map2 _ _ _ _ = raise ListPair.UnequalLengths;
   23.41 -
   23.42 -fun fold_map3 _ [] [] [] acc = ([], acc)
   23.43 -  | fold_map3 f (x1::x1s) (x2::x2s) (x3::x3s) acc =
   23.44 -    let
   23.45 -      val (x, acc') = f x1 x2 x3 acc;
   23.46 -      val (xs, acc'') = fold_map3 f x1s x2s x3s acc';
   23.47 -    in (x :: xs, acc'') end
   23.48 -  | fold_map3 _ _ _ _ _ = raise ListPair.UnequalLengths;
   23.49 -
   23.50  fun seq_conds f n k xs =
   23.51    if k = n then
   23.52      map (f false) (take (k - 1) xs)
   23.53 @@ -174,10 +138,10 @@
   23.54  fun mk_TFrees n = mk_TFrees' (replicate n @{sort type});
   23.55  
   23.56  fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
   23.57 -fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
   23.58 +fun mk_Freess' x Tss = @{fold_map 2} mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
   23.59  
   23.60  fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts);
   23.61 -fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss;
   23.62 +fun mk_Freess x Tss = @{fold_map 2} mk_Frees (mk_names (length Tss) x) Tss;
   23.63  
   23.64  fun dest_TFree_or_TVar (TFree sS) = sS
   23.65    | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S)
   23.66 @@ -191,7 +155,7 @@
   23.67  fun variant_types ss Ss ctxt =
   23.68    let
   23.69      val (tfrees, _) =
   23.70 -      fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt);
   23.71 +      @{fold_map 2} (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt);
   23.72      val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
   23.73    in (tfrees, ctxt') end;
   23.74  
    24.1 --- a/src/HOL/Tools/Function/function_core.ML	Wed Oct 08 14:34:30 2014 +0200
    24.2 +++ b/src/HOL/Tools/Function/function_core.ML	Wed Oct 08 17:09:07 2014 +0200
    24.3 @@ -873,7 +873,7 @@
    24.4      val cert = cterm_of (Proof_Context.theory_of lthy)
    24.5  
    24.6      val xclauses = PROFILE "xclauses"
    24.7 -      (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
    24.8 +      (@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
    24.9          RCss GIntro_thms) RIntro_thmss
   24.10  
   24.11      val complete =
    25.1 --- a/src/HOL/Tools/Function/function_lib.ML	Wed Oct 08 14:34:30 2014 +0200
    25.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Wed Oct 08 17:09:07 2014 +0200
    25.3 @@ -11,10 +11,6 @@
    25.4  
    25.5    val dest_all_all: term -> term list * term
    25.6  
    25.7 -  val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
    25.8 -  val map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) -> 'a list -> 'b list -> 'c list ->
    25.9 -    'd list -> 'e list -> 'f list -> 'g list -> 'h list
   25.10 -
   25.11    val unordered_pairs: 'a list -> ('a * 'a) list
   25.12  
   25.13    val rename_bound: string -> term -> term
   25.14 @@ -50,14 +46,6 @@
   25.15    | dest_all_all t = ([],t)
   25.16  
   25.17  
   25.18 -fun map4 f = Ctr_Sugar_Util.map4 f
   25.19 -
   25.20 -fun map7 _ [] [] [] [] [] [] [] = []
   25.21 -  | map7 f (x :: xs) (y :: ys) (z :: zs) (u :: us) (v :: vs) (w :: ws) (b :: bs) = f x y z u v w b :: map7 f xs ys zs us vs ws bs
   25.22 -  | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
   25.23 -
   25.24 -
   25.25 -
   25.26  (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
   25.27  fun unordered_pairs [] = []
   25.28    | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
    26.1 --- a/src/HOL/Tools/Function/mutual.ML	Wed Oct 08 14:34:30 2014 +0200
    26.2 +++ b/src/HOL/Tools/Function/mutual.ML	Wed Oct 08 17:09:07 2014 +0200
    26.3 @@ -106,7 +106,7 @@
    26.4          (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew)
    26.5        end
    26.6  
    26.7 -    val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num))
    26.8 +    val (parts, rews) = split_list (@{map 4} define fs caTss resultTs (1 upto num))
    26.9  
   26.10      fun convert_eqs (f, qs, gs, args, rhs) =
   26.11        let
    27.1 --- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Wed Oct 08 14:34:30 2014 +0200
    27.2 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Wed Oct 08 17:09:07 2014 +0200
    27.3 @@ -57,7 +57,8 @@
    27.4        ||>> mk_TFrees live
    27.5        ||>> mk_TFrees (dead_of_bnf bnf)
    27.6      val argTss = map2 (fn a => fn b => [mk_pred2T a a, a --> b, b --> a,mk_pred2T a b]) As Bs
    27.7 -    val ((argss, argss'), ctxt) = fold_map2 mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss) ctxt
    27.8 +    val ((argss, argss'), ctxt) =
    27.9 +      @{fold_map 2} mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss) ctxt
   27.10        |>> `transpose
   27.11     
   27.12      val assms = map (mk_Quotient #> HOLogic.mk_Trueprop) argss
    28.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Oct 08 14:34:30 2014 +0200
    28.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Oct 08 17:09:07 2014 +0200
    28.3 @@ -1319,7 +1319,7 @@
    28.4            construct_value ctxt
    28.5                (if new_s = @{type_name prod} then @{const_name Pair}
    28.6                 else @{const_name PairBox}, new_Ts ---> new_T)
    28.7 -              (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
    28.8 +              (@{map 3} (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
    28.9                      [t1, t2])
   28.10          | t' => raise TERM ("Nitpick_HOL.coerce_term", [t'])
   28.11        else
    29.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Oct 08 14:34:30 2014 +0200
    29.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Oct 08 17:09:07 2014 +0200
    29.3 @@ -602,7 +602,7 @@
    29.4          val old_rs = map2 (#kk_project_seq kk r) old_offsets old_arities
    29.5        in
    29.6          fold1 (#kk_product kk)
    29.7 -              (map3 (rel_expr_from_rel_expr kk) Rs Rs' old_rs)
    29.8 +              (@{map 3} (rel_expr_from_rel_expr kk) Rs Rs' old_rs)
    29.9        end
   29.10      else
   29.11        lone_rep_fallback kk (Struct Rs) old_R r
    30.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Oct 08 14:34:30 2014 +0200
    30.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Oct 08 17:09:07 2014 +0200
    30.3 @@ -508,7 +508,7 @@
    30.4            val k2 = k div k1
    30.5          in
    30.6            list_comb (HOLogic.pair_const T1 T2,
    30.7 -                     map3 (fn T => term_for_atom seen T T) [T1, T2]
    30.8 +                     @{map 3} (fn T => term_for_atom seen T T) [T1, T2]
    30.9                            (* ### k2 or k1? FIXME *)
   30.10                            [j div k2, j mod k2] [k1, k2])
   30.11          end
   30.12 @@ -578,7 +578,7 @@
   30.13                    if length arg_Ts = 0 then
   30.14                      []
   30.15                    else
   30.16 -                    map3 (fn Ts => term_for_rep true seen Ts Ts) arg_Ts arg_Rs
   30.17 +                    @{map 3} (fn Ts => term_for_rep true seen Ts Ts) arg_Ts arg_Rs
   30.18                           arg_jsss
   30.19                      |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
   30.20                      |> dest_n_tuple (length uncur_arg_Ts)
   30.21 @@ -633,7 +633,7 @@
   30.22            val (js1, js2) = chop arity1 js
   30.23          in
   30.24            list_comb (HOLogic.pair_const T1 T2,
   30.25 -                     map3 (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2]
   30.26 +                     @{map 3} (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2]
   30.27                            [[js1], [js2]])
   30.28          end
   30.29        | term_for_rep _ seen T T' (Vect (k, R')) [js] =
    31.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Oct 08 14:34:30 2014 +0200
    31.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Oct 08 17:09:07 2014 +0200
    31.3 @@ -700,7 +700,7 @@
    31.4          (mk_quasi_clauses res_aa aa1 aa2))
    31.5  
    31.6  fun add_connective_frames conn mk_quasi_clauses res_frame frame1 frame2 =
    31.7 -  fold I (map3 (fn (_, res_aa) => fn (_, aa1) => fn (_, aa2) =>
    31.8 +  fold I (@{map 3} (fn (_, res_aa) => fn (_, aa1) => fn (_, aa2) =>
    31.9                     add_connective_var conn mk_quasi_clauses res_aa aa1 aa2)
   31.10                 res_frame frame1 frame2)
   31.11  
    32.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Oct 08 14:34:30 2014 +0200
    32.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Oct 08 17:09:07 2014 +0200
    32.3 @@ -1151,7 +1151,7 @@
    32.4                                              (j :: js, pool)
    32.5                                            end)
    32.6                                  ([], pool)
    32.7 -        val ws' = map3 (fn j => fn x => fn T =>
    32.8 +        val ws' = @{map 3} (fn j => fn x => fn T =>
    32.9                             constr ((1, j), T, Atom x,
   32.10                                     nick ^ " [" ^ string_of_int j ^ "]"))
   32.11                         (rev js) atom_schema type_schema
    33.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Oct 08 14:34:30 2014 +0200
    33.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Oct 08 17:09:07 2014 +0200
    33.3 @@ -439,7 +439,7 @@
    33.4                  s_let Ts "l" (n + 1) dataT bool_T
    33.5                        (fn t1 =>
    33.6                            discriminate_value hol_ctxt x t1 ::
    33.7 -                          map3 (sel_eq Ts x t1) (index_seq 0 n) arg_Ts args
    33.8 +                          @{map 3} (sel_eq Ts x t1) (index_seq 0 n) arg_Ts args
    33.9                            |> foldr1 s_conj) t1
   33.10              else
   33.11                raise SAME ()
    34.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Oct 08 14:34:30 2014 +0200
    34.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Oct 08 17:09:07 2014 +0200
    34.3 @@ -39,7 +39,6 @@
    34.4    val all_permutations : 'a list -> 'a list list
    34.5    val chunk_list : int -> 'a list -> 'a list list
    34.6    val chunk_list_unevenly : int list -> 'a list -> 'a list list
    34.7 -  val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
    34.8    val double_lookup :
    34.9      ('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option
   34.10    val triple_lookup :
   34.11 @@ -202,10 +201,6 @@
   34.12    | chunk_list_unevenly (k :: ks) xs =
   34.13      let val (xs1, xs2) = chop k xs in xs1 :: chunk_list_unevenly ks xs2 end
   34.14  
   34.15 -fun map3 _ [] [] [] = []
   34.16 -  | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
   34.17 -  | map3 _ _ _ _ = raise ListPair.UnequalLengths
   34.18 -
   34.19  fun double_lookup eq ps key =
   34.20    case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps
   34.21                      (SOME key) of
    35.1 --- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Oct 08 14:34:30 2014 +0200
    35.2 +++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Oct 08 17:09:07 2014 +0200
    35.3 @@ -38,7 +38,7 @@
    35.4  
    35.5      val selss = if has_duplicates (op aconv) (flat selss0) then [] else selss0
    35.6    in
    35.7 -    Ctr_Sugar_Util.fold_map2 mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt
    35.8 +    @{fold_map 2} mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt
    35.9      |>> (pair T #> single)
   35.10    end
   35.11  
    36.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Wed Oct 08 14:34:30 2014 +0200
    36.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Wed Oct 08 17:09:07 2014 +0200
    36.3 @@ -217,14 +217,14 @@
    36.4                    val time_slice = time_mult (1.0 / Real.fromInt (length labels)) (reference_time l)
    36.5                    val timeouts =
    36.6                      map (adjust_merge_timeout preplay_timeout o curry Time.+ time_slice) times0
    36.7 -                  val meths_outcomess = map3 (preplay_isar_step ctxt) timeouts hopelesses succs'
    36.8 +                  val meths_outcomess = @{map 3} (preplay_isar_step ctxt) timeouts hopelesses succs'
    36.9                  in
   36.10                    (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of
   36.11                      NONE => steps
   36.12                    | SOME times =>
   36.13                      (* "l" successfully eliminated *)
   36.14                      (decrement_step_count ();
   36.15 -                     map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data)
   36.16 +                     @{map 3} (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data)
   36.17                         times succs' meths_outcomess;
   36.18                       map (replace_successor l labels) lfs;
   36.19                       steps_before @ update_steps succs' steps_after))
    37.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Oct 08 14:34:30 2014 +0200
    37.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Oct 08 17:09:07 2014 +0200
    37.3 @@ -8,7 +8,6 @@
    37.4  sig
    37.5    val sledgehammerN : string
    37.6    val log2 : real -> real
    37.7 -  val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
    37.8    val app_hd : ('a -> 'a) -> 'a list -> 'a list
    37.9    val plural_s : int -> string
   37.10    val serial_commas : string -> string list -> string list
   37.11 @@ -39,8 +38,6 @@
   37.12  val log10_2 = Math.log10 2.0
   37.13  fun log2 n = Math.log10 n / log10_2
   37.14  
   37.15 -fun map3 xs = Ctr_Sugar_Util.map3 xs
   37.16 -
   37.17  fun app_hd f (x :: xs) = f x :: xs
   37.18  
   37.19  fun plural_s n = if n = 1 then "" else "s"
    38.1 --- a/src/HOL/Tools/coinduction.ML	Wed Oct 08 14:34:30 2014 +0200
    38.2 +++ b/src/HOL/Tools/coinduction.ML	Wed Oct 08 17:09:07 2014 +0200
    38.3 @@ -73,7 +73,7 @@
    38.4            val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
    38.5              |>> (fn names => Variable.variant_fixes names names_ctxt) ;
    38.6            val eqs =
    38.7 -            map3 (fn name => fn T => fn (_, rhs) =>
    38.8 +            @{map 3} (fn name => fn T => fn (_, rhs) =>
    38.9                HOLogic.mk_eq (Free (name, T), rhs))
   38.10              names Ts raw_eqs;
   38.11            val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems
    39.1 --- a/src/Pure/ML/ml_antiquotations.ML	Wed Oct 08 14:34:30 2014 +0200
    39.2 +++ b/src/Pure/ML/ml_antiquotations.ML	Wed Oct 08 17:09:07 2014 +0200
    39.3 @@ -167,6 +167,70 @@
    39.4          in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
    39.5  
    39.6  
    39.7 +(* basic combinators *)
    39.8 +
    39.9 +local
   39.10 +
   39.11 +val parameter = Parse.position Parse.nat >> (fn (n, pos) =>
   39.12 +  if n > 1 then n else error ("Bad parameter: " ^ string_of_int n ^ Position.here pos));
   39.13 +
   39.14 +fun indices n = map string_of_int (1 upto n);
   39.15 +
   39.16 +fun empty n = replicate_string n " []";
   39.17 +fun dummy n = replicate_string n " _";
   39.18 +fun vars x n = implode (map (fn a => " " ^ x ^ a) (indices n));
   39.19 +fun cons n = implode (map (fn a => " (x" ^ a ^ " :: xs" ^ a ^ ")") (indices n));
   39.20 +
   39.21 +val tuple = enclose "(" ")" o commas;
   39.22 +fun tuple_empty n = tuple (replicate n "[]");
   39.23 +fun tuple_vars x n = tuple (map (fn a => x ^ a) (indices n));
   39.24 +fun tuple_cons n = "(" ^ tuple_vars "x" n ^ " :: xs)"
   39.25 +fun cons_tuple n = tuple (map (fn a => "x" ^ a ^ " :: xs" ^ a) (indices n));
   39.26 +
   39.27 +in
   39.28 +
   39.29 +val _ = Theory.setup
   39.30 + (ML_Antiquotation.value @{binding map}
   39.31 +    (Scan.lift parameter >> (fn n =>
   39.32 +      "fn f =>\n\
   39.33 +      \  let\n\
   39.34 +      \    fun map _" ^ empty n ^ " = []\n\
   39.35 +      \      | map f" ^ cons n ^ " = f" ^ vars "x" n ^ " :: map f" ^ vars "xs" n ^ "\n\
   39.36 +      \      | map _" ^  dummy n ^ " = raise ListPair.UnequalLengths\n" ^
   39.37 +      "  in map f end")) #>
   39.38 +  ML_Antiquotation.value @{binding fold}
   39.39 +    (Scan.lift parameter >> (fn n =>
   39.40 +      "fn f =>\n\
   39.41 +      \  let\n\
   39.42 +      \    fun fold _" ^ empty n ^ " a = a\n\
   39.43 +      \      | fold f" ^ cons n ^ " a = fold f" ^ vars "xs" n ^ " (f" ^ vars "x" n ^ " a)\n\
   39.44 +      \      | fold _" ^  dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^
   39.45 +      "  in fold f end")) #>
   39.46 +  ML_Antiquotation.value @{binding fold_map}
   39.47 +    (Scan.lift parameter >> (fn n =>
   39.48 +      "fn f =>\n\
   39.49 +      \  let\n\
   39.50 +      \    fun fold_map _" ^ empty n ^ " a = ([], a)\n\
   39.51 +      \      | fold_map f" ^ cons n ^ " a =\n\
   39.52 +      \          let\n\
   39.53 +      \            val (x, a') = f" ^ vars "x" n ^ " a\n\
   39.54 +      \            val (xs, a'') = fold_map f" ^ vars "xs" n ^ " a'\n\
   39.55 +      \          in (x :: xs, a'') end\n\
   39.56 +      \      | fold_map _" ^  dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^
   39.57 +      "  in fold_map f end")) #>
   39.58 +  ML_Antiquotation.value @{binding split_list}
   39.59 +    (Scan.lift parameter >> (fn n =>
   39.60 +      "fn list =>\n\
   39.61 +      \  let\n\
   39.62 +      \    fun split_list [] =" ^ tuple_empty n ^ "\n\
   39.63 +      \      | split_list" ^ tuple_cons n ^ " =\n\
   39.64 +      \          let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\
   39.65 +      \          in " ^ cons_tuple n ^ "end\n\
   39.66 +      \  in split_list list end")))
   39.67 +
   39.68 +end;
   39.69 +
   39.70 +
   39.71  (* outer syntax *)
   39.72  
   39.73  fun with_keyword f =