src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

     ((Binding.qualify true base (Binding.name thmN), []),
      map_index (fn (i, thm) => ([thm], f_attrs i)) thms));
 
 fun massage_multi_notes b_names Ts =
   maps (fn (thmN, thmss, attrs) =>
-    map3 (fn b_name => fn Type (T_name, _) => fn thms =>
+    @{map 3} (fn b_name => fn Type (T_name, _) => fn thms =>
         ((Binding.qualify true b_name (Binding.name thmN), attrs T_name), [(thms, [])]))
       b_names Ts thmss)
   #> filter_out (null o fst o hd o snd);
 
 fun derive_map_set_rel_thms plugins fp live As Bs abs_inverses ctr_defs' fp_nesting_set_maps

           val goals =
             if n = 0 then
               []
             else
               [mk_Trueprop_eq (build_rel_app names_lthy Rs [] ta tb,
-                 (case flat (map5 (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of
+                 (case flat (@{map 5} (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of
                    [] => @{term True}
                  | conjuncts => Library.foldr1 HOLogic.mk_conj conjuncts))];
 
           fun prove goal =
             Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>

                     map2 (HOLogic.mk_Trueprop oo build_rel_app lthy Rs []) argAs argBs,
                   thesis)),
                names_ctxt)
             end;
 
-          val (assms, names_lthy) = fold_map2 mk_assms ctrAs ctrBs names_lthy;
+          val (assms, names_lthy) = @{fold_map 2} mk_assms ctrAs ctrBs names_lthy;
           val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis);
           val thm =
             Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
               mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust injects
                 rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs)

                 else (map (Logic.mk_implies o pair (HOLogic.mk_Trueprop prem)) concls, ctxt')
               else
                 ([], ctxt)
             end;
           val (goals, names_lthy) = apfst (flat o flat o flat)
-            (fold_map2 (fn disc =>
+            (@{fold_map 2} (fn disc =>
                  fold_map (fn sel => fold_map (mk_goal disc sel) setAs))
                discAs selAss names_lthy);
         in
           if null goals then
             []

 
 fun mk_recs_args_types ctr_Tsss Cs absTs repTs ns mss ctor_rec_fun_Ts lthy =
   let
     val Css = map2 replicate ns Cs;
     val x_Tssss =
-      map6 (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_rec_fun_T =>
+      @{map 6} (fn absT => fn repT => fn n => fn ms => fn ctr_Tss => fn ctor_rec_fun_T =>
           map2 (map2 unzip_recT)
             ctr_Tss (dest_absumprodT absT repT n ms (domain_type ctor_rec_fun_T)))
         absTs repTs ns mss ctr_Tsss ctor_rec_fun_Ts;
 
     val x_Tsss' = map (map flat_rec_arg_args) x_Tssss;

 
 fun mk_corec_fun_arg_types0 ctr_Tsss Cs absTs repTs ns mss fun_Ts =
   let
     val ctr_Tsss' = map repair_nullary_single_ctr ctr_Tsss;
     val g_absTs = map range_type fun_Ts;
-    val g_Tsss = map repair_nullary_single_ctr (map5 dest_absumprodT absTs repTs ns mss g_absTs);
-    val g_Tssss = map3 (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT)))
+    val g_Tsss = map repair_nullary_single_ctr (@{map 5} dest_absumprodT absTs repTs ns mss g_absTs);
+    val g_Tssss = @{map 3} (fn C => map2 (map2 (map (curry (op -->) C) oo unzip_corecT)))
       Cs ctr_Tsss' g_Tsss;
     val q_Tssss = map (map (map (fn [_] => [] | [_, T] => [mk_pred1T (domain_type T)]))) g_Tssss;
   in
     (q_Tssss, g_Tsss, g_Tssss, g_absTs)
   end;

     fun build_dtor_corec_arg _ [] [cg] = cg
       | build_dtor_corec_arg T [cq] [cg, cg'] =
         mk_If cq (build_sum_inj Inl_const (fastype_of cg, T) $ cg)
           (build_sum_inj Inr_const (fastype_of cg', T) $ cg');
 
-    val pgss = map3 flat_corec_preds_predsss_gettersss pss qssss gssss;
+    val pgss = @{map 3} flat_corec_preds_predsss_gettersss pss qssss gssss;
     val cqssss = map2 (map o map o map o rapp) cs qssss;
     val cgssss = map2 (map o map o map o rapp) cs gssss;
-    val cqgsss = map3 (map3 (map3 build_dtor_corec_arg)) g_Tsss cqssss cgssss;
+    val cqgsss = @{map 3} (@{map 3} (@{map 3} build_dtor_corec_arg)) g_Tsss cqssss cgssss;
   in
     ((x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types)), lthy)
   end;
 
 fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy =

     val (ctor_rec_absTs, fpT) = strip_typeN nn (fastype_of ctor_rec)
       |>> map domain_type ||> domain_type;
   in
     define_co_rec_as Least_FP Cs fpT (mk_binding recN)
       (fold_rev (fold_rev Term.lambda) fss (Term.list_comb (ctor_rec,
-         map4 (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
+         @{map 4} (fn ctor_rec_absT => fn rep => fn fs => fn xsss =>
              mk_case_absumprod ctor_rec_absT rep fs (map (map HOLogic.mk_tuple) xsss)
                (map flat_rec_arg_args xsss))
            ctor_rec_absTs reps fss xssss)))
   end;
 

     val nn = length fpTs;
     val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec)));
   in
     define_co_rec_as Greatest_FP Cs fpT (mk_binding corecN)
       (fold_rev (fold_rev Term.lambda) pgss (Term.list_comb (dtor_corec,
-         map5 mk_preds_getterss_join cs cpss f_absTs abss cqgsss)))
+         @{map 5} mk_preds_getterss_join cs cpss f_absTs abss cqgsss)))
   end;
 
 fun postproc_co_induct lthy nn prop prop_conj =
   Drule.zero_var_indexes
   #> `(conj_dests nn)

           fold_rev Logic.all (argAs @ argBs) (fold_rev (curry Logic.mk_implies)
             (map2 (HOLogic.mk_Trueprop oo build_rel_app names_lthy (Rs @ IRs) fpA_Ts) argAs argBs)
             (HOLogic.mk_Trueprop (build_rel_app names_lthy (Rs @ IRs) fpA_Ts
               (Term.list_comb (ctrA, argAs)) (Term.list_comb (ctrB, argBs)))));
       in
-        flat (map4 (map4 mk_prem) ctrAss ctrBss ctrAsss ctrBsss)
+        flat (@{map 4} (@{map 4} mk_prem) ctrAss ctrBss ctrAsss ctrBsss)
       end;
 
     val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
       (map2 (build_the_rel [] lthy (Rs @ IRs) []) fpA_Ts fpB_Ts) IRs));
 

           in (xs, pprems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs))) end;
 
         fun mk_prem (xs, raw_pprems, concl) =
           fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl));
 
-        val raw_premss = map4 (map3 o mk_raw_prem) ps ctrss ctr_Tsss ctrXs_Tsss;
+        val raw_premss = @{map 4} (@{map 3} o mk_raw_prem) ps ctrss ctr_Tsss ctrXs_Tsss;
 
         val goal =
           Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
             HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) ps us)));
 

             in
               build_map lthy [] build_simple (T, U) $ x
             end;
 
         val fxsss = map2 (map2 (flat_rec_arg_args oo map2 (map o build_rec))) xsss x_Tssss;
-        val goalss = map5 (map4 o mk_goal) frecs xctrss fss xsss fxsss;
-
-        val tacss = map4 (map ooo
+        val goalss = @{map 5} (@{map 4} o mk_goal) frecs xctrss fss xsss fxsss;
+
+        val tacss = @{map 4} (map ooo
               mk_rec_tac pre_map_defs (fp_nesting_map_ident0s @ live_nesting_map_ident0s) rec_defs)
             ctor_rec_thms fp_abs_inverses abs_inverses ctr_defss;
 
         fun prove goal tac =
           Goal.prove_sorry lthy [] [] goal (tac o #context)

         flat (map2 append disc_concls ctr_concls)
       end;
 
     val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
     val coinduct_conclss =
-      map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
+      @{map 3} (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
 
     val common_coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes nn));
     val coinduct_consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
 
     val coinduct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names coinduct_cases));

               (if n = 1 then [] else [discA_t, discB_t],
                Library.foldr1 HOLogic.mk_conj
                  (map2 (build_rel_app lthy (Rs @ IRs) fpA_Ts) selA_ts selB_ts))]);
 
         fun mk_prem_concl n discA_ts selA_tss discB_ts selB_tss =
-          Library.foldr1 HOLogic.mk_conj (flat (map5 (mk_prem_ctr_concls n)
+          Library.foldr1 HOLogic.mk_conj (flat (@{map 5} (mk_prem_ctr_concls n)
             (1 upto n) discA_ts selA_tss discB_ts selB_tss))
           handle List.Empty => @{term True};
 
         fun mk_prem IR tA tB n discA_ts selA_tss discB_ts selB_tss =
           fold_rev Logic.all [tA, tB] (Logic.mk_implies (HOLogic.mk_Trueprop (IR $ tA $ tB),
             HOLogic.mk_Trueprop (mk_prem_concl n discA_ts selA_tss discB_ts selB_tss)));
       in
-        map8 mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss
+        @{map 8} mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss
       end;
 
     val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
       IRs (map2 (build_the_rel [] lthy (Rs @ IRs) []) fpA_Ts fpB_Ts)));
 

     corecs corec_defs export_args lthy =
   let
     fun mk_ctor_dtor_corec_thm dtor_inject dtor_ctor corec =
       iffD1 OF [dtor_inject, trans OF [corec, dtor_ctor RS sym]];
 
-    val ctor_dtor_corec_thms = map3 mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms;
+    val ctor_dtor_corec_thms =
+      @{map 3} mk_ctor_dtor_corec_thm dtor_injects dtor_ctors dtor_corec_thms;
 
     val nn = length pre_bnfs;
 
     val pre_map_defs = map map_def_of_bnf pre_bnfs;
     val pre_rel_defs = map rel_def_of_bnf pre_bnfs;

     val vdiscss = map2 (map o rapp) vs discss;
     val vselsss = map2 (map o map o rapp) vs selsss;
 
     val coinduct_thms_pairs =
       let
-        val uvrs = map3 (fn r => fn u => fn v => r $ u $ v) rs us vs;
+        val uvrs = @{map 3} (fn r => fn u => fn v => r $ u $ v) rs us vs;
         val uv_eqs = map2 (curry HOLogic.mk_eq) us vs;
         val strong_rs =
-          map4 (fn u => fn v => fn uvr => fn uv_eq =>
+          @{map 4} (fn u => fn v => fn uvr => fn uv_eq =>
             fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs;
 
         fun build_the_rel rs' T Xs_T =
           build_rel [] lthy [] (fn (_, X) => nth rs' (find_index (curry (op =) X) Xs)) (T, Xs_T)
           |> Term.subst_atomic_types (Xs ~~ fpTs);

           (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @
           (if null usels then
              []
            else
              [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc],
-                Library.foldr1 HOLogic.mk_conj (map3 (build_rel_app rs') usels vsels ctrXs_Ts))]);
+                Library.foldr1 HOLogic.mk_conj (@{map 3} (build_rel_app rs') usels vsels ctrXs_Ts))]);
 
         fun mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss =
-          Library.foldr1 HOLogic.mk_conj (flat (map6 (mk_prem_ctr_concls rs' n)
+          Library.foldr1 HOLogic.mk_conj (flat (@{map 6} (mk_prem_ctr_concls rs' n)
             (1 upto n) udiscs uselss vdiscs vselss ctrXs_Tss))
           handle List.Empty => @{term True};
 
         fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss ctrXs_Tss =
           fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr,
             HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss ctrXs_Tss)));
 
         val concl =
           HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-            (map3 (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v)))
+            (@{map 3} (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v)))
                uvrs us vs));
 
         fun mk_goal rs' =
-          Logic.list_implies (map9 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss
+          Logic.list_implies (@{map 9} (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss
             ctrXs_Tsss, concl);
 
         val goals = map mk_goal [rs, strong_rs];
 
         fun prove dtor_coinduct' goal =

             else
               cqg
           end;
 
         val cqgsss' = map (map (map build_corec)) cqgsss;
-        val goalss = map8 (map4 oooo mk_goal) cs cpss gcorecs ns kss ctrss mss cqgsss';
+        val goalss = @{map 8} (@{map 4} oooo mk_goal) cs cpss gcorecs ns kss ctrss mss cqgsss';
 
         val tacss =
-          map4 (map ooo mk_corec_tac corec_defs live_nesting_map_ident0s)
+          @{map 4} (map ooo mk_corec_tac corec_defs live_nesting_map_ident0s)
             ctor_dtor_corec_thms pre_map_defs abs_inverses ctr_defss;
 
         fun prove goal tac =
           Goal.prove_sorry lthy [] [] goal (tac o #context)
           |> Thm.close_derivation;

         fun mk_goal c cps gcorec n k disc =
           mk_Trueprop_eq (disc $ (gcorec $ c),
             if n = 1 then @{const True}
             else Library.foldr1 HOLogic.mk_conj (seq_conds mk_maybe_not n k cps));
 
-        val goalss = map6 (map2 oooo mk_goal) cs cpss gcorecs ns kss discss;
+        val goalss = @{map 6} (map2 oooo mk_goal) cs cpss gcorecs ns kss discss;
 
         fun mk_case_split' cp = Drule.instantiate' [] [SOME (certify lthy cp)] @{thm case_split};
 
         val case_splitss' = map (map mk_case_split') cpss;
 
-        val tacss = map3 (map oo mk_corec_disc_iff_tac) case_splitss' corec_thmss disc_thmsss;
+        val tacss = @{map 3} (map oo mk_corec_disc_iff_tac) case_splitss' corec_thmss disc_thmsss;
 
         fun prove goal tac =
           Goal.prove_sorry lthy [] [] goal (tac o #context)
           |> singleton export_args
           |> singleton (Proof_Context.export names_lthy lthy)

       in
         corec_thm RS arg_cong' RS sel_thm'
       end;
 
     fun mk_corec_sel_thms corec_thmss =
-      map3 (map3 (map2 o mk_corec_sel_thm)) corec_thmss selsss sel_thmsss;
+      @{map 3} (@{map 3} (map2 o mk_corec_sel_thm)) corec_thmss selsss sel_thmsss;
 
     val corec_sel_thmsss = mk_corec_sel_thms corec_thmss;
   in
     ((coinduct_thms_pairs,
       mk_coinduct_attrs fpTs (map #ctrs ctr_sugars) (map #discs ctr_sugars) mss),

         warning "Map function and relator names ignored"
       else
         ();
 
     val Bs =
-      map3 (fn alive => fn A as TFree (_, S) => fn B =>
+      @{map 3} (fn alive => fn A as TFree (_, S) => fn B =>
           if alive then resort_tfree_or_tvar S B else A)
         (liveness_of_fp_bnf num_As any_fp_bnf) As Bs0;
 
     val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
 

 
         val maybe_conceal_def_binding = Thm.def_binding
           #> not (Config.get no_defs_lthy bnf_note_all) ? Binding.conceal;
 
         val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
-          |> apfst split_list o fold_map3 (fn b => fn mx => fn rhs =>
+          |> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs =>
               Local_Theory.define ((b, mx), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd)
             ctr_bindings ctr_mixfixes ctr_rhss
           ||> `Local_Theory.restore;
 
         val phi = Proof_Context.export_morphism lthy lthy';

             val sel_default_lthy = fake_local_theory_for_sel_defaults sel_bTs lthy;
 
             val sel_default_eqs = map (prepare_term sel_default_lthy) raw_sel_default_eqs;
 
             fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs);
-            val ctr_specs = map3 ctr_spec_of disc_bindings ctrs0 sel_bindingss;
+            val ctr_specs = @{map 3} ctr_spec_of disc_bindings ctrs0 sel_bindingss;
 
             val (ctr_sugar as {case_cong, ...}, lthy') =
               free_constructors tacss ((((plugins, discs_sels), standard_binding), ctr_specs),
                 sel_default_eqs) lthy
 

          #> massage_res, lthy')
       end;
 
     fun wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types (wrap_one_etc, lthy) =
       fold_map I wrap_one_etc lthy
-      |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list15 o split_list)
+      |>> apsnd split_list o apfst (apsnd @{split_list 4} o apfst @{split_list 15} o split_list)
         o split_list;
 
     fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects
         rel_distincts set_thmss =
       injects @ distincts @ case_thms @ co_recs @ map_thms @ rel_injects @ rel_distincts @

               ((map single rel_induct_thms, single common_rel_induct_thm),
                (rel_induct_attrs, rel_induct_attrs))
             end;
 
         val simp_thmss =
-          map6 mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss;
+          @{map 6} mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss;
 
         val common_notes =
           (if nn > 1 then
              [(inductN, [induct_thm], K induct_attrs),
               (rel_inductN, common_rel_induct_thms, K common_rel_induct_attrs)]

             (map #exhaust ctr_sugars) (flat pre_set_defss) (flat ctr_defss)
             dtor_ctors abs_inverses
           |> split_list;
 
         val simp_thmss =
-          map6 mk_simp_thms ctr_sugars
-            (map3 flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss)
+          @{map 6} mk_simp_thms ctr_sugars
+            (@{map 3} flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss)
             map_thmss rel_injectss rel_distinctss set_thmss;
 
         val common_notes =
           (set_inductN, set_induct_thms, nth set_induct_attrss) ::
           (if nn > 1 then