# HG changeset patch
# User wenzelm
# Date 1412780947 -7200
# Node ID 9f10d82e81880ecb947f144812dcc24702a0cb21
# Parent  8529745af3dccd4b9d0abf6f854878b6c9e4f473
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};

diff -r 8529745af3dc -r 9f10d82e8188 NEWS
--- a/NEWS	Wed Oct 08 14:34:30 2014 +0200
+++ b/NEWS	Wed Oct 08 17:09:07 2014 +0200
@@ -137,6 +137,9 @@
 * Tactical PARALLEL_ALLGOALS is the most common way to refer to
 PARALLEL_GOALS.
 
+* Basic combinators map, fold, fold_map, split_list are available as
+parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
+
 
 *** System ***
 
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Library/bnf_lfp_countable.ML
--- a/src/HOL/Library/bnf_lfp_countable.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -58,7 +58,7 @@
 
 fun mk_encode_injectives_tac ctxt ns induct nchotomys injectss recss map_comps' inj_map_strongs' =
   HEADGOAL (rtac induct) THEN
-  EVERY (map4 (fn n => fn nchotomy => fn injects => fn recs =>
+  EVERY (@{map 4} (fn n => fn nchotomy => fn injects => fn recs =>
       mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs')
     ns nchotomys injectss recss);
 
@@ -166,7 +166,7 @@
 
       val (xs, names_ctxt) = ctxt |> mk_Frees "x" fpTs;
 
-      val conjuncts = map3 mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0);
+      val conjuncts = @{map 3} mk_conjunct fpTs xs (mk_encode_funs ctxt fpTs ns ctrss0 recs0);
       val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj conjuncts);
     in
       Goal.prove (*no sorry*) ctxt [] [] goal (fn {context = ctxt, prems = _} =>
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -154,12 +154,12 @@
       ||>> mk_Frees "A" (map HOLogic.mk_setT As)
       ||>> mk_Frees "x" As;
 
-    val CAs = map3 mk_T_of_bnf Dss Ass_repl inners;
+    val CAs = @{map 3} mk_T_of_bnf Dss Ass_repl inners;
     val CCA = mk_T_of_bnf oDs CAs outer;
-    val CBs = map3 mk_T_of_bnf Dss Bss_repl inners;
+    val CBs = @{map 3} mk_T_of_bnf Dss Bss_repl inners;
     val outer_sets = mk_sets_of_bnf (replicate olive oDs) (replicate olive CAs) outer;
-    val inner_setss = map3 mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners;
-    val inner_bds = map3 mk_bd_of_bnf Dss Ass_repl inners;
+    val inner_setss = @{map 3} mk_sets_of_bnf (map (replicate ilive) Dss) (replicate olive Ass) inners;
+    val inner_bds = @{map 3} mk_bd_of_bnf Dss Ass_repl inners;
     val outer_bd = mk_bd_of_bnf oDs CAs outer;
 
     (*%f1 ... fn. outer.map (inner_1.map f1 ... fn) ... (inner_m.map f1 ... fn)*)
@@ -280,7 +280,7 @@
           val single_set_bd_thmss =
             map ((fn f => map f (0 upto olive - 1)) o single_set_bd_thm) (0 upto ilive - 1);
         in
-          map3 (fn set'_eq_set => fn set_alt => fn single_set_bds => fn ctxt =>
+          @{map 3} (fn set'_eq_set => fn set_alt => fn single_set_bds => fn ctxt =>
             mk_comp_set_bd_tac ctxt set'_eq_set bd_ordIso_natLeq_thm_opt set_alt single_set_bds)
           set'_eq_sets set_alt_thms single_set_bd_thmss
         end;
@@ -320,7 +320,7 @@
     val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
 
     val inner_witss = map (map (fn (I, wit) => Term.list_comb (wit, map (nth xs) I)))
-      (map3 (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As))
+      (@{map 3} (fn Ds => fn n => mk_wits_of_bnf (replicate n Ds) (replicate n As))
         Dss inwitss inners);
 
     val inner_witsss = map (map (nth inner_witss) o fst) outer_wits;
@@ -637,7 +637,7 @@
     val before_kill_dest = map2 append kill_poss live_poss;
     val kill_ns = map length kill_poss;
     val (inners', accum') =
-      fold_map5 (fn i => permute_and_kill (qualify i))
+      @{fold_map 5} (fn i => permute_and_kill (qualify i))
         (if length bnfs = 1 then [0] else (1 upto length bnfs))
         kill_ns before_kill_src before_kill_dest bnfs accum;
 
@@ -649,7 +649,7 @@
     val after_lift_src = map2 append new_poss old_poss;
     val lift_ns = map (fn xs => length As - length xs) Ass';
   in
-    ((kill_poss, As), fold_map5 (fn i => lift_and_permute (qualify i))
+    ((kill_poss, As), @{fold_map 5} (fn i => lift_and_permute (qualify i))
       (if length bnfs = 1 then [0] else 1 upto length bnfs)
       lift_ns after_lift_src after_lift_dest inners' accum')
   end;
@@ -667,7 +667,7 @@
     val ((kill_poss, As), (inners', ((cache', unfold_set'), lthy'))) =
       normalize_bnfs qualify Ass Ds flatten_tyargs inners accum;
 
-    val Ds = oDs @ flat (map3 (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss);
+    val Ds = oDs @ flat (@{map 3} (uncurry append oo curry swap oo map o nth) tfreess kill_poss Dss);
     val As = map TFree As;
   in
     apfst (rpair (Ds, As))
@@ -931,7 +931,7 @@
             val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
             val ((inners, (Dss, Ass)), (accum', lthy')) =
               apfst (apsnd split_list o split_list)
-                (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) flatten_tyargs Xs Ds0)
+                (@{fold_map 2} (fn i => bnf_of_typ Smart_Inline (qualify i) flatten_tyargs Xs Ds0)
                 (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' accum);
           in
             compose_bnf const_policy qualify flatten_tyargs bnf inners oDs Dss Ass (accum', lthy')
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -864,7 +864,7 @@
     val CA = mk_bnf_T Ds As Calpha;
     val CR = mk_bnf_T Ds RTs Calpha;
     val setRs =
-      map3 (fn R => fn T => fn U =>
+      @{map 3} (fn R => fn T => fn U =>
           HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split R) Rs As Bs;
 
     (*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO
@@ -1057,7 +1057,7 @@
 
     val map_cong0_goal =
       let
-        val prems = map4 (mk_map_cong_prem Logic.mk_implies x) zs bnf_sets_As fs fs_copy;
+        val prems = @{map 4} (mk_map_cong_prem Logic.mk_implies x) zs bnf_sets_As fs fs_copy;
         val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
           Term.list_comb (bnf_map_AsBs, fs_copy) $ x);
       in
@@ -1074,7 +1074,7 @@
             fold_rev Logic.all fs (mk_Trueprop_eq (set_comp_map, image_comp_set))
           end;
       in
-        map3 mk_goal bnf_sets_As bnf_sets_Bs fs
+        @{map 3} mk_goal bnf_sets_As bnf_sets_Bs fs
       end;
 
     val card_order_bd_goal = HOLogic.mk_Trueprop (mk_card_order bnf_bd_As);
@@ -1185,7 +1185,7 @@
         fun mk_map_cong mk_implies () =
           let
             val prem0 = mk_Trueprop_eq (x, x_copy);
-            val prems = map4 (mk_map_cong_prem mk_implies x_copy) zs bnf_sets_As fs fs_copy;
+            val prems = @{map 4} (mk_map_cong_prem mk_implies x_copy) zs bnf_sets_As fs fs_copy;
             val eq = mk_Trueprop_eq (Term.list_comb (bnf_map_AsBs, fs) $ x,
               Term.list_comb (bnf_map_AsBs, fs_copy) $ x_copy);
             val goal = fold_rev Logic.all (x :: x_copy :: fs @ fs_copy)
@@ -1364,7 +1364,7 @@
                   (mk_Ball (setB $ y) (Term.absfree (dest_Free b)
                     (HOLogic.mk_imp (R $ a $ b, S $ a $ b))))));
             val prems = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs) $ x $ y) ::
-              map6 mk_prem bnf_sets_As bnf_sets_Bs Rs Rs_copy zs ys;
+              @{map 6} mk_prem bnf_sets_As bnf_sets_Bs Rs Rs_copy zs ys;
             val concl = HOLogic.mk_Trueprop (Term.list_comb (rel, Rs_copy) $ x $ y);
           in
             Goal.prove_sorry lthy [] []
@@ -1389,9 +1389,9 @@
               [Term.list_comb (relCsBs, S_CsBs) $ (Term.list_comb (bnf_map_AsCs, is) $ x) $ y,
                Term.list_comb (relAsCs, S_AsCs) $ x $ (Term.list_comb (bnf_map_BsCs, gs) $ y)];
             val rhss =
-              [Term.list_comb (rel, map3 (fn f => fn P => fn T =>
+              [Term.list_comb (rel, @{map 3} (fn f => fn P => fn T =>
                  mk_vimage2p f (HOLogic.id_const T) $ P) is S_CsBs Bs') $ x $ y,
-               Term.list_comb (rel, map3 (fn f => fn P => fn T =>
+               Term.list_comb (rel, @{map 3} (fn f => fn P => fn T =>
                  mk_vimage2p (HOLogic.id_const T) f $ P) gs S_AsCs As') $ x $ y];
             val goals = map2 mk_goal lhss rhss;
           in
@@ -1451,7 +1451,7 @@
           let
             val rel_sets = map2 (fn A => fn B => mk_rel 1 [A] [B] @{term rel_set}) As' Bs';
             val rel_Rs = Term.list_comb (rel, Rs);
-            val goals = map4 (fn R => fn rel_set => fn setA => fn setB => HOLogic.mk_Trueprop
+            val goals = @{map 4} (fn R => fn rel_set => fn setA => fn setB => HOLogic.mk_Trueprop
               (mk_rel_fun rel_Rs (rel_set $ R) $ setA $ setB)) Rs rel_sets bnf_sets_As bnf_sets_Bs;
           in
             if null goals then []
@@ -1468,7 +1468,7 @@
 
         fun mk_inj_map_strong () =
           let
-            val assms = map5 (fn setA => fn z => fn f => fn z' => fn f' =>
+            val assms = @{map 5} (fn setA => fn z => fn f => fn z' => fn f' =>
               fold_rev Logic.all [z, z']
                 (Logic.mk_implies (mk_Trueprop_mem (z, setA $ x),
                    Logic.mk_implies (mk_Trueprop_mem (z', setA $ x'),
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -524,7 +524,7 @@
 
 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);
@@ -788,7 +788,7 @@
               []
             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))];
 
@@ -824,7 +824,7 @@
                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 = _} =>
@@ -968,7 +968,7 @@
                 ([], 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
@@ -1072,7 +1072,7 @@
   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;
@@ -1100,8 +1100,8 @@
   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
@@ -1139,10 +1139,10 @@
         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;
@@ -1200,7 +1200,7 @@
   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)))
@@ -1213,7 +1213,7 @@
   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 =
@@ -1256,7 +1256,7 @@
             (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
@@ -1354,7 +1354,7 @@
         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,
@@ -1402,9 +1402,9 @@
             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 goalss = @{map 5} (@{map 4} o mk_goal) frecs xctrss fss xsss fxsss;
 
-        val tacss = map4 (map ooo
+        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;
 
@@ -1441,7 +1441,7 @@
 
     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));
@@ -1506,7 +1506,7 @@
                  (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};
 
@@ -1514,7 +1514,7 @@
           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
@@ -1632,7 +1632,8 @@
     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;
 
@@ -1667,10 +1668,10 @@
 
     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 =
@@ -1686,10 +1687,10 @@
              []
            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};
 
@@ -1699,11 +1700,11 @@
 
         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];
@@ -1757,10 +1758,10 @@
           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 =
@@ -1778,13 +1779,13 @@
             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)
@@ -1815,7 +1816,7 @@
       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
@@ -1997,7 +1998,7 @@
         ();
 
     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;
 
@@ -2044,7 +2045,7 @@
           #> 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;
@@ -2103,7 +2104,7 @@
             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),
@@ -2136,7 +2137,7 @@
 
     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
@@ -2204,7 +2205,7 @@
             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
@@ -2315,8 +2316,8 @@
           |> 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 =
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -141,7 +141,7 @@
 
 fun mk_ctor_iff_dtor_tac ctxt cTs cctor cdtor ctor_dtor dtor_ctor =
   HEADGOAL (rtac iffI THEN'
-    EVERY' (map3 (fn cTs => fn cx => fn th =>
+    EVERY' (@{map 3} (fn cTs => fn cx => fn th =>
       dtac (Drule.instantiate' cTs [NONE, NONE, SOME cx] arg_cong) THEN'
       SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN'
       atac) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor]));
@@ -212,7 +212,7 @@
   end;
 
 fun mk_corec_disc_iff_tac case_splits' corecs discs ctxt =
-  EVERY (map3 (fn case_split_tac => fn corec_thm => fn disc =>
+  EVERY (@{map 3} (fn case_split_tac => fn corec_thm => fn disc =>
       HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [corec_thm] THEN
       HEADGOAL (asm_simp_tac (ss_only basic_simp_thms ctxt)) THEN
       (if is_refl disc then all_tac else HEADGOAL (rtac disc)))
@@ -277,7 +277,7 @@
 
     fun mk_unfold_prop_tac dtor_corec_transfer corec_def =
       mk_unfold_corec_type_tac dtor_corec_transfer corec_def THEN
-      EVERY (map4 mk_unfold_type_tac type_definitions pss qssss gssss);
+      EVERY (@{map 4} mk_unfold_type_tac type_definitions pss qssss gssss);
   in
     HEADGOAL Goal.conjunction_tac THEN
     EVERY (map2 mk_unfold_prop_tac dtor_corec_transfers corec_defs)
@@ -315,7 +315,7 @@
      else
        unfold_thms_tac ctxt ctr_defs) THEN
     HEADGOAL (rtac ctor_induct') THEN co_induct_inst_as_projs_tac ctxt 0 THEN
-    EVERY (map4 (EVERY oooo map3 o
+    EVERY (@{map 4} (EVERY oooo @{map 3} o
         mk_induct_discharge_prem_tac ctxt nn n fp_abs_inverses abs_inverses set_maps)
       pre_set_defss mss (unflat mss (1 upto n)) kkss)
   end;
@@ -348,7 +348,7 @@
     EVERY' ([rtac allI, rtac allI, rtac impI, select_prem_tac nn (dtac meta_spec) kk,
         dtac meta_spec, dtac meta_mp, atac, rtac exhaust, K (co_induct_inst_as_projs_tac ctxt 0),
         hyp_subst_tac ctxt] @
-      map4 (fn k => fn ctr_def => fn discs => fn sels =>
+      @{map 4} (fn k => fn ctr_def => fn discs => fn sels =>
         EVERY' ([rtac exhaust, K (co_induct_inst_as_projs_tac ctxt 1)] @
           map2 (fn k' => fn discs' =>
             if k' = k then
@@ -361,7 +361,7 @@
 fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs fp_abs_inverses abs_inverses
     dtor_ctors exhausts ctr_defss discsss selsss =
   HEADGOAL (rtac dtor_coinduct' THEN'
-    EVERY' (map10 (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn)
+    EVERY' (@{map 10} (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn)
       (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
       selsss));
 
@@ -401,7 +401,7 @@
 fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss
     dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses nesting_rel_eqs =
   rtac dtor_rel_coinduct 1 THEN
-   EVERY (map11 (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
+   EVERY (@{map 11} (fn ct => fn assm => fn exhaust => fn discs => fn sels => fn ctor_defs =>
      fn dtor_ctor => fn ctor_inject => fn abs_inject => fn rel_pre_def => fn abs_inverse =>
       (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW
          (dtac (rotate_prems ~1 (cterm_instantiate_pos [NONE, NONE, NONE, NONE, SOME ct]
@@ -420,7 +420,7 @@
 
 fun mk_rel_induct0_tac ctxt ctor_rel_induct assms cterms exhausts ctor_defss ctor_injects
     rel_pre_list_defs Abs_inverses nesting_rel_eqs =
-  rtac ctor_rel_induct 1 THEN EVERY (map6 (fn cterm => fn exhaust => fn ctor_defs =>
+  rtac ctor_rel_induct 1 THEN EVERY (@{map 6} (fn cterm => fn exhaust => fn ctor_defs =>
       fn ctor_inject => fn rel_pre_list_def => fn Abs_inverse =>
         HEADGOAL (rtac exhaust THEN_ALL_NEW (rtac exhaust THEN_ALL_NEW
           (rtac (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -125,8 +125,8 @@
     val xTs = map (domain_type o fastype_of) xtors;
     val yTs = map (domain_type o fastype_of) xtor's;
 
-    val absAs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss;
-    val absBs = map3 (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss;
+    val absAs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allAs) Dss bnfs abss;
+    val absBs = @{map 3} (fn Ds => mk_abs o mk_T_of_bnf Ds allBs) Dss bnfs abss;
     val fp_repAs = map2 mk_rep absATs fp_reps;
     val fp_repBs = map2 mk_rep absBTs fp_reps;
 
@@ -186,7 +186,7 @@
     val fp_or_nesting_rel_monos = map rel_mono_of_bnf fp_or_nesting_bnfs;
 
     val xtor_rel_co_induct =
-      mk_xtor_rel_co_induct_thm fp (map3 cast castAs castBs pre_rels) pre_phis rels phis xs ys
+      mk_xtor_rel_co_induct_thm fp (@{map 3} cast castAs castBs pre_rels) pre_phis rels phis xs ys
         xtors xtor's (mk_rel_xtor_co_induct_tactic fp abs_inverses rel_xtor_co_inducts rel_defs
           rel_monos fp_or_nesting_rel_eqs fp_or_nesting_rel_monos)
         lthy;
@@ -268,7 +268,7 @@
         val subst = Term.typ_subst_atomic fold_thetaAs;
 
         fun mk_fp_absT_repT fp_repT fp_absT = mk_absT thy fp_repT fp_absT ooo mk_repT;
-        val mk_fp_absT_repTs = map5 mk_fp_absT_repT fp_repTs fp_absTs absTs repTs;
+        val mk_fp_absT_repTs = @{map 5} mk_fp_absT_repT fp_repTs fp_absTs absTs repTs;
 
         val fold_preTs' = mk_fp_absT_repTs (map subst fold_preTs);
 
@@ -411,7 +411,7 @@
                 fp_abs fp_rep abs rep rhs)
           end;
 
-        val goals = map8 mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps;
+        val goals = @{map 8} mk_goals recs xtors rec_strs pre_rec_maps fp_abss fp_reps abss reps;
 
         val pre_map_defs = no_refl (map map_def_of_bnf bnfs);
         val fp_pre_map_defs = no_refl (map map_def_of_bnf pre_bnfs);
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -205,7 +205,7 @@
       | freeze_fpTs_call _ _ _ T = T;
 
     val ctr_Tsss = map (map binder_types) ctr_Tss;
-    val ctrXs_Tsss = map4 (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss;
+    val ctrXs_Tsss = @{map 4} (map2 o map2 oo freeze_fpTs_call) kks fpTs callssss ctr_Tsss;
     val ctrXs_repTs = map mk_sumprodT_balanced ctrXs_Tsss;
 
     val ns = map length ctr_Tsss;
@@ -261,7 +261,7 @@
         fun mk_binding b pre = Binding.prefix_name (pre ^ "_") b;
 
         val ((co_recs, co_rec_defs), lthy) =
-          fold_map2 (fn b =>
+          @{fold_map 2} (fn b =>
               if fp = Least_FP then define_rec (the recs_args_types) (mk_binding b) fpTs Cs reps
               else define_corec (the corecs_args_types) (mk_binding b) fpTs Cs abss)
             fp_bs xtor_co_recs lthy
@@ -340,9 +340,9 @@
           |> morph_fp_sugar phi;
 
         val target_fp_sugars =
-          map16 mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss ctr_sugars
-            co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss co_rec_disc_thmss
-            co_rec_sel_thmsss fp_sugars0;
+          @{map 16} mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss
+            ctr_sugars co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss
+            co_rec_disc_thmss co_rec_sel_thmsss fp_sugars0;
 
         val n2m_sugar = (target_fp_sugars, fp_sugar_thms);
       in
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -32,7 +32,7 @@
     val folded_C_IHs = map (fn thm => thm RS @{thm spec2} RS mp) raw_C_IHs;
     val C_IHs = map2 (curry op |>) folded_C_IHs unfolds;
     val C_IH_monos =
-      map3 (fn C_IH => fn mono => fn unfold =>
+      @{map 3} (fn C_IH => fn mono => fn unfold =>
         (mono RSN (2, @{thm vimage2p_mono}), C_IH)
         |> fp = Greatest_FP ? swap
         |> op RS
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -433,7 +433,7 @@
   if xs = [x] then f else HOLogic.tupled_lambda x (Term.list_comb (f, xs));
 
 fun mk_case_absumprod absT rep fs xss xss' =
-  HOLogic.mk_comp (mk_case_sumN_balanced (map3 mk_tupled_fun fs (map mk_tuple_balanced xss) xss'),
+  HOLogic.mk_comp (mk_case_sumN_balanced (@{map 3} mk_tupled_fun fs (map mk_tuple_balanced xss) xss'),
     mk_rep absT rep);
 
 fun If_const T = Const (@{const_name If}, HOLogic.boolT --> T --> T --> T);
@@ -512,7 +512,7 @@
     fun mk_prem pre_relphi phi x y xtor xtor' =
       HOLogic.mk_Trueprop (list_all_free [x, y] (flip (curry HOLogic.mk_imp)
         (pre_relphi $ (dtor xtor x) $ (dtor xtor' y)) (phi $ (ctor xtor x) $ (ctor xtor' y))));
-    val prems = map6 mk_prem pre_relphis pre_phis xs ys xtors xtor's;
+    val prems = @{map 6} mk_prem pre_relphis pre_phis xs ys xtors xtor's;
 
     val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
       (map2 (flip mk_leq) relphis pre_phis));
@@ -531,7 +531,7 @@
     val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_ophis;
     fun mk_transfer relphi pre_phi un_fold un_fold' =
       fold_rev mk_rel_fun arg_rels (flip mk_rel_fun relphi pre_phi) $ un_fold $ un_fold';
-    val transfers = map4 mk_transfer relphis pre_ophis un_folds un_folds';
+    val transfers = @{map 4} mk_transfer relphis pre_ophis un_folds un_folds';
 
     val goal = fold_rev Logic.all (phis @ pre_ophis)
       (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers));
@@ -565,7 +565,7 @@
     val rewrite1s = mk_rewrites map_cong1s;
     val rewrite2s = mk_rewrites map_cong2s;
     val unique_prems =
-      map4 (fn xtor_map => fn un_fold => fn rewrite1 => fn rewrite2 =>
+      @{map 4} (fn xtor_map => fn un_fold => fn rewrite1 => fn rewrite2 =>
         mk_trans (rewrite_comp_comp2 OF [xtor_map, un_fold])
           (mk_trans rewrite1 (mk_sym rewrite2)))
       xtor_maps xtor_un_folds rewrite1s rewrite2s;
@@ -613,7 +613,8 @@
 
     val ((bnfs, (deadss, livess)), accum) =
       apfst (apsnd split_list o split_list)
-        (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs
+        (@{fold_map 2}
+          (fn b => bnf_of_typ Smart_Inline (raw_qualify b) flatten_tyargs Xs Ds0) bs rhsXs
           ((empty_comp_cache, empty_unfolds), lthy));
 
     fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))
@@ -631,13 +632,13 @@
     val ((kill_poss, _), (bnfs', ((_, unfold_set'), lthy'))) =
       normalize_bnfs norm_qualify Ass Ds (K (resBs' @ Xs)) bnfs accum;
 
-    val Dss = map3 (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
+    val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
 
     fun pre_qualify b = Binding.qualify false (Binding.name_of b)
       #> not (Config.get lthy' bnf_note_all) ? Binding.conceal;
 
     val ((pre_bnfs, (deadss, absT_infos)), lthy'') =
-      fold_map4 (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
+      @{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
         bs (not (null live_phantoms) :: replicate (nn - 1) false) Dss bnfs' lthy'
       |>> split_list
       |>> apsnd split_list;
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -138,21 +138,21 @@
     val sum_sTs = map2 (fn T => fn U => T --> U) activeAs sumFTs;
 
     (* terms *)
-    val mapsAsAs = map4 mk_map_of_bnf Dss Ass Ass bnfs;
-    val mapsAsBs = map4 mk_map_of_bnf Dss Ass Bss bnfs;
-    val mapsBsCs' = map4 mk_map_of_bnf Dss Bss Css' bnfs;
-    val mapsAsCs' = map4 mk_map_of_bnf Dss Ass Css' bnfs;
-    val map_Inls = map4 mk_map_of_bnf Dss Bss (replicate n (passiveAs @ sumBsAs)) bnfs;
-    val map_Inls_rev = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ sumBsAs)) Bss bnfs;
-    val map_fsts = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Ass bnfs;
-    val map_snds = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Bss bnfs;
-    fun mk_setss Ts = map3 mk_sets_of_bnf (map (replicate live) Dss)
+    val mapsAsAs = @{map 4} mk_map_of_bnf Dss Ass Ass bnfs;
+    val mapsAsBs = @{map 4} mk_map_of_bnf Dss Ass Bss bnfs;
+    val mapsBsCs' = @{map 4} mk_map_of_bnf Dss Bss Css' bnfs;
+    val mapsAsCs' = @{map 4} mk_map_of_bnf Dss Ass Css' bnfs;
+    val map_Inls = @{map 4} mk_map_of_bnf Dss Bss (replicate n (passiveAs @ sumBsAs)) bnfs;
+    val map_Inls_rev = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ sumBsAs)) Bss bnfs;
+    val map_fsts = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Ass bnfs;
+    val map_snds = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ RTs)) Bss bnfs;
+    fun mk_setss Ts = @{map 3} mk_sets_of_bnf (map (replicate live) Dss)
       (map (replicate live) (replicate n Ts)) bnfs;
     val setssAs = mk_setss allAs;
     val setssAs' = transpose setssAs;
     val bis_setss = mk_setss (passiveAs @ RTs);
-    val relsAsBs = map4 mk_rel_of_bnf Dss Ass Bss bnfs;
-    val bds = map3 mk_bd_of_bnf Dss Ass bnfs;
+    val relsAsBs = @{map 4} mk_rel_of_bnf Dss Ass Bss bnfs;
+    val bds = @{map 3} mk_bd_of_bnf Dss Ass bnfs;
     val sum_bd = Library.foldr1 (uncurry mk_csum) bds;
     val sum_bdT = fst (dest_relT (fastype_of sum_bd));
     val (sum_bdT_params, sum_bdT_params') = `(map TFree) (Term.add_tfreesT sum_bdT []);
@@ -244,7 +244,7 @@
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
-    val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
+    val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
 
     (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>
       map id ... id f(m+1) ... f(m+n) x = x*)
@@ -253,7 +253,7 @@
         fun mk_prem set f z z' =
           HOLogic.mk_Trueprop
             (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
-        val prems = map4 mk_prem (drop m sets) self_fs zs zs';
+        val prems = @{map 4} mk_prem (drop m sets) self_fs zs zs';
         val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
       in
         Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
@@ -262,7 +262,7 @@
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
-    val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
+    val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
     val in_mono'_thms = map (fn thm =>
       (thm OF (replicate m subset_refl)) RS @{thm set_mp}) in_monos;
 
@@ -271,7 +271,8 @@
         val prems = map2 (curry mk_Trueprop_eq) yFs yFs_copy;
         val maps = map (fn mapx => Term.list_comb (mapx, all_gs)) mapsBsCs';
         val concls =
-          map3 (fn x => fn y => fn mapx => mk_Trueprop_eq (mapx $ x, mapx $ y)) yFs yFs_copy maps;
+          @{map 3} (fn x => fn y => fn mapx => mk_Trueprop_eq (mapx $ x, mapx $ y))
+            yFs yFs_copy maps;
         val goals = map2 (fn prem => fn concl => Logic.mk_implies (prem, concl)) prems concls;
       in
         map (fn goal =>
@@ -290,11 +291,11 @@
     (*forall i = 1 ... n: (\<forall>x \<in> Bi. si \<in> Fi_in UNIV .. UNIV B1 ... Bn)*)
     val coalg_spec =
       let
-        val ins = map3 mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs;
+        val ins = @{map 3} mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs;
         fun mk_coalg_conjunct B s X z z' =
           mk_Ball B (Term.absfree z' (HOLogic.mk_mem (s $ z, X)));
 
-        val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_coalg_conjunct Bs ss ins zs zs')
+        val rhs = Library.foldr1 HOLogic.mk_conj (@{map 5} mk_coalg_conjunct Bs ss ins zs zs')
       in
         fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs
       end;
@@ -328,7 +329,7 @@
         fun mk_prem x B = mk_Trueprop_mem (x, B);
         fun mk_concl s x B set = HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) B);
         val prems = map2 mk_prem zs Bs;
-        val conclss = map3 (fn s => fn x => fn sets => map2 (mk_concl s x) Bs (drop m sets))
+        val conclss = @{map 3} (fn s => fn x => fn sets => map2 (mk_concl s x) Bs (drop m sets))
           ss zs setssAs;
         val goalss = map2 (fn prem => fn concls => map (fn concl =>
           Logic.list_implies (coalg_prem :: [prem], concl)) concls) prems conclss;
@@ -371,8 +372,8 @@
           mk_Ball B (Term.absfree z' (HOLogic.mk_eq
             (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ z]), s' $ (f $ z))));
         val rhs = HOLogic.mk_conj
-          (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'),
-           Library.foldr1 HOLogic.mk_conj (map7 mk_mor Bs mapsAsBs fs ss s's zs zs'))
+          (Library.foldr1 HOLogic.mk_conj (@{map 5} mk_fbetw fs Bs B's zs zs'),
+           Library.foldr1 HOLogic.mk_conj (@{map 7} mk_mor Bs mapsAsBs fs ss s's zs zs'))
       in
         fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs
       end;
@@ -402,11 +403,11 @@
         val prem = HOLogic.mk_Trueprop (mk_mor Bs ss B's s's fs);
         fun mk_image_goal f B1 B2 =
           Logic.mk_implies (prem, HOLogic.mk_Trueprop (mk_leq (mk_image f $ B1) B2));
-        val image_goals = map3 mk_image_goal fs Bs B's;
+        val image_goals = @{map 3} mk_image_goal fs Bs B's;
         fun mk_elim_goal B mapAsBs f s s' x =
           Logic.list_implies ([prem, mk_Trueprop_mem (x, B)],
             mk_Trueprop_eq (Term.list_comb (mapAsBs, passive_ids @ fs @ [s $ x]), s' $ (f $ x)));
-        val elim_goals = map6 mk_elim_goal Bs mapsAsBs fs ss s's zs;
+        val elim_goals = @{map 6} mk_elim_goal Bs mapsAsBs fs ss s's zs;
         fun prove goal =
           Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def))
           |> Thm.close_derivation
@@ -462,7 +463,7 @@
             (HOLogic.mk_comp (Term.list_comb (mapAsBs, passive_ids @ fs), s),
             HOLogic.mk_comp (s', f));
         val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
-        val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
+        val rhs = Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct mapsAsBs fs ss s's);
       in
         Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
           (K (mk_mor_UNIV_tac morE_thms mor_def))
@@ -484,7 +485,7 @@
 
     val mor_case_sum_thm =
       let
-        val maps = map3 (fn s => fn sum_s => fn mapx =>
+        val maps = @{map 3} (fn s => fn sum_s => fn mapx =>
           mk_case_sum (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ Inls), s), sum_s))
           s's sum_ss map_Inls;
       in
@@ -503,7 +504,7 @@
     val bis_def_bind = (Thm.def_binding bis_bind, []);
 
     fun mk_bis_le_conjunct R B1 B2 = mk_leq R (mk_Times (B1, B2));
-    val bis_le = Library.foldr1 HOLogic.mk_conj (map3 mk_bis_le_conjunct Rs Bs B's)
+    val bis_le = Library.foldr1 HOLogic.mk_conj (@{map 3} mk_bis_le_conjunct Rs Bs B's)
 
     val bis_spec =
       let
@@ -519,7 +520,7 @@
 
         val rhs = HOLogic.mk_conj
           (bis_le, Library.foldr1 HOLogic.mk_conj
-            (map9 mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss))
+            (@{map 9} mk_bis Rs ss s's zs z's RFs map_fsts map_snds bis_setss))
       in
         fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ Rs) rhs
       end;
@@ -563,7 +564,7 @@
 
         val rhs = HOLogic.mk_conj
           (bis_le, Library.foldr1 HOLogic.mk_conj
-            (map6 mk_conjunct Rs ss s's zs z's relsAsBs))
+            (@{map 6} mk_conjunct Rs ss s's zs z's relsAsBs))
       in
         Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs))
           (K (mk_bis_rel_tac m bis_def in_rels map_comps map_cong0s set_mapss))
@@ -684,7 +685,7 @@
         fun mk_concl i R = HOLogic.mk_Trueprop (mk_leq R (mk_lsbis Bs ss i));
         val goals = map2 (fn i => fn R => Logic.mk_implies (sbis_prem, mk_concl i R)) ks sRs;
       in
-        map3 (fn goal => fn i => fn def =>
+        @{map 3} (fn goal => fn i => fn def =>
           Goal.prove_sorry lthy [] [] goal (K (mk_incl_lsbis_tac n i def))
           |> Thm.close_derivation
           |> singleton (Proof_Context.export names_lthy lthy)) goals ks lsbis_defs
@@ -695,7 +696,7 @@
         fun mk_concl i B = HOLogic.mk_Trueprop (mk_equiv B (mk_lsbis Bs ss i));
         val goals = map2 (fn i => fn B => Logic.mk_implies (coalg_prem, mk_concl i B)) ks Bs;
       in
-        map3 (fn goal => fn l_incl => fn incl_l =>
+        @{map 3} (fn goal => fn l_incl => fn incl_l =>
           Goal.prove_sorry lthy [] [] goal
             (K (mk_equiv_lsbis_tac sbis_lsbis_thm l_incl incl_l
               bis_Id_on_thm bis_converse_thm bis_O_thm))
@@ -755,7 +756,7 @@
           fun mk_set_sbd i bd_Card_order bds =
             map (fn thm => @{thm ordLeq_ordIso_trans} OF
               [bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds;
-          val set_sbdss = map3 mk_set_sbd ks bd_Card_orders set_bdss;
+          val set_sbdss = @{map 3} mk_set_sbd ks bd_Card_orders set_bdss;
        in
          (lthy, sbd, sbdT, sbd_card_order, sbd_Cinfinite, sbd_Card_order, set_sbdss)
        end;
@@ -765,7 +766,7 @@
     val sum_sbd_listT = HOLogic.listT sum_sbdT;
     val sum_sbd_list_setT = HOLogic.mk_setT sum_sbd_listT;
     val bdTs = passiveAs @ replicate n sbdT;
-    val to_sbd_maps = map4 mk_map_of_bnf Dss Ass (replicate n bdTs) bnfs;
+    val to_sbd_maps = @{map 4} mk_map_of_bnf Dss Ass (replicate n bdTs) bnfs;
     val bdFTs = mk_FTs bdTs;
     val sbdFT = mk_sumTN bdFTs;
     val treeT = HOLogic.mk_prodT (sum_sbd_list_setT, sum_sbd_listT --> sbdFT);
@@ -773,15 +774,15 @@
     val treeTs = passiveAs @ replicate n treeT;
     val treeQTs = passiveAs @ replicate n treeQT;
     val treeFTs = mk_FTs treeTs;
-    val tree_maps = map4 mk_map_of_bnf Dss (replicate n bdTs) (replicate n treeTs) bnfs;
-    val final_maps = map4 mk_map_of_bnf Dss (replicate n treeTs) (replicate n treeQTs) bnfs;
+    val tree_maps = @{map 4} mk_map_of_bnf Dss (replicate n bdTs) (replicate n treeTs) bnfs;
+    val final_maps = @{map 4} mk_map_of_bnf Dss (replicate n treeTs) (replicate n treeQTs) bnfs;
     val isNode_setss = mk_setss (passiveAs @ replicate n sbdT);
 
     val root = HOLogic.mk_set sum_sbd_listT [HOLogic.mk_list sum_sbdT []];
     val Zero = HOLogic.mk_tuple (map (fn U => absdummy U root) activeAs);
     val Lev_recT = fastype_of Zero;
 
-    val Nil = HOLogic.mk_tuple (map3 (fn i => fn z => fn z'=>
+    val Nil = HOLogic.mk_tuple (@{map 3} (fn i => fn z => fn z'=>
       Term.absfree z' (mk_InN activeAs z i)) ks zs zs');
     val rv_recT = fastype_of Nil;
 
@@ -812,7 +813,7 @@
     val isNodeT =
       Library.foldr (op -->) (map fastype_of [Kl, lab, kl], HOLogic.boolT);
 
-    val Succs = map3 (fn i => fn k => fn k' =>
+    val Succs = @{map 3} (fn i => fn k => fn k' =>
       HOLogic.mk_Collect (fst k', snd k', HOLogic.mk_mem (mk_InN sbdTs k i, mk_Succ Kl kl)))
       ks kks kks';
 
@@ -828,7 +829,7 @@
 
     val ((isNode_frees, (_, isNode_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> fold_map3 (fn i => fn x => fn sets => Local_Theory.define
+      |> @{fold_map 3} (fn i => fn x => fn sets => Local_Theory.define
         ((isNode_bind i, NoSyn), (isNode_def_bind i, isNode_spec sets x i)))
         ks xs isNode_setss
       |>> apsnd split_list o split_list
@@ -848,7 +849,7 @@
         val empty = HOLogic.mk_mem (HOLogic.mk_list sum_sbdT [], Kl);
 
         val tree = mk_Ball Kl (Term.absfree kl'
-          (Library.foldr1 HOLogic.mk_conj (map4 (fn Succ => fn i => fn k => fn k' =>
+          (Library.foldr1 HOLogic.mk_conj (@{map 4} (fn Succ => fn i => fn k => fn k' =>
             mk_Ball Succ (Term.absfree k' (mk_isNode
               (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i])) i)))
           Succs ks kks kks')));
@@ -889,7 +890,7 @@
           let val in_k = mk_InN sbdTs k i;
           in Term.absfree k' (HOLogic.mk_prod (mk_Shift Kl in_k, mk_shift lab in_k)) end;
 
-        val f = Term.list_comb (mapFT, passive_ids @ map3 mk_f ks kks kks');
+        val f = Term.list_comb (mapFT, passive_ids @ @{map 3} mk_f ks kks kks');
         val (fTs1, fTs2) = apsnd tl (chop (i - 1) (map (fn T => T --> FT) bdFTs));
         val fs = map mk_undefined fTs1 @ (f :: map mk_undefined fTs2);
       in
@@ -899,7 +900,7 @@
 
     val ((strT_frees, (_, strT_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> fold_map3 (fn i => fn mapFT => fn FT => Local_Theory.define
+      |> @{fold_map 3} (fn i => fn mapFT => fn FT => Local_Theory.define
         ((strT_bind i, NoSyn), (strT_def_bind i, strT_spec mapFT FT i)))
         ks tree_maps treeFTs
       |>> apsnd split_list o split_list
@@ -955,11 +956,11 @@
                   (HOLogic.mk_conj (Cons, HOLogic.mk_conj (b_set, kl_rec))))
               end;
           in
-            Term.absfree a' (Library.foldl1 mk_union (map3 mk_set ks sets zs_copy))
+            Term.absfree a' (Library.foldl1 mk_union (@{map 3} mk_set ks sets zs_copy))
           end;
 
         val Suc = Term.absdummy HOLogic.natT (Term.absfree Lev_rec'
-          (HOLogic.mk_tuple (map5 mk_Suc ks ss setssAs zs zs')));
+          (HOLogic.mk_tuple (@{map 5} mk_Suc ks ss setssAs zs zs')));
 
         val rhs = mk_rec_nat Zero Suc;
       in
@@ -1002,7 +1003,7 @@
           end;
 
         val Cons = Term.absfree sumx' (Term.absdummy sum_sbd_listT (Term.absfree rv_rec'
-          (HOLogic.mk_tuple (map4 mk_Cons ks ss zs zs'))));
+          (HOLogic.mk_tuple (@{map 4} mk_Cons ks ss zs zs'))));
 
         val rhs = mk_rec_list Nil Cons;
       in
@@ -1043,7 +1044,7 @@
             (Term.list_comb (to_sbd_map, passive_ids @ map (mk_to_sbd s k i) ks) $ (s $ k)) i);
 
         val Lab = Term.absfree kl'
-          (mk_case_sumN (map5 mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z));
+          (mk_case_sumN (@{map 5} mk_case ks to_sbd_maps ss zs zs') $ (mk_rv ss kl i $ z));
 
         val rhs = HOLogic.mk_prod (mk_UNION (HOLogic.mk_UNIV HOLogic.natT)
           (Term.absfree nat' (mk_Lev ss nat i $ z)), Lab);
@@ -1053,7 +1054,7 @@
 
     val ((beh_frees, (_, beh_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> fold_map2 (fn i => fn z =>
+      |> @{fold_map 2} (fn i => fn z =>
         Local_Theory.define ((beh_bind i, NoSyn), (beh_def_bind i, beh_spec i z))) ks zs
       |>> apsnd split_list o split_list
       ||> `Local_Theory.restore;
@@ -1141,11 +1142,12 @@
                       mk_Lev ss (HOLogic.mk_Suc nat) i $ z));
               in
                 HOLogic.mk_imp (HOLogic.mk_eq (mk_rv ss kl i $ z, mk_InN activeAs z' i'),
-                  (Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct'' ks (drop m sets) zs_copy2)))
+                  (Library.foldr1 HOLogic.mk_conj
+                    (@{map 3} mk_conjunct'' ks (drop m sets) zs_copy2)))
               end;
           in
             HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z),
-              Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct' ks setssAs ss zs_copy))
+              Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct' ks setssAs ss zs_copy))
           end;
 
         val goal = list_all_free (kl :: zs @ zs_copy @ zs_copy2)
@@ -1180,7 +1182,7 @@
                 HOLogic.mk_imp (HOLogic.mk_mem
                   (mk_append (kl, HOLogic.mk_list sum_sbdT [mk_InN sbdTs k i']),
                     mk_Lev ss (HOLogic.mk_Suc nat) i $ z),
-                  (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct'' ks sets ss zs_copy)))
+                  (Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct'' ks sets ss zs_copy)))
               end;
           in
             HOLogic.mk_imp (HOLogic.mk_mem (kl, mk_Lev ss nat i $ z),
@@ -1238,9 +1240,9 @@
           HOLogic.mk_Trueprop (mk_congruent R (HOLogic.mk_comp
             (Term.list_comb (final_map, passive_ids @ map mk_proj lsbisAs), strT)));
 
-        val goals = map3 mk_goal lsbisAs final_maps strTAs;
+        val goals = @{map 3} mk_goal lsbisAs final_maps strTAs;
       in
-        map4 (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 =>
+        @{map 4} (fn goal => fn lsbisE => fn map_comp_id => fn map_cong0 =>
           Goal.prove_sorry lthy [] [] goal
             (K (mk_congruent_str_final_tac m lsbisE map_comp_id map_cong0 equiv_LSBIS_thms))
           |> Thm.close_derivation)
@@ -1265,7 +1267,7 @@
 
     val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
       lthy
-      |> fold_map4 (fn b => fn mx => fn car_final => fn in_car_final =>
+      |> @{fold_map 4} (fn b => fn mx => fn car_final => fn in_car_final =>
         typedef (b, params, mx) car_final NONE
           (EVERY' [rtac exI, rtac in_car_final] 1)) bs mixfixes car_finals in_car_final_thms
       |>> apsnd split_list o split_list;
@@ -1323,7 +1325,7 @@
 
     val ((dtor_frees, (_, dtor_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> fold_map6 (fn i => fn rep => fn str => fn mapx => fn Jz => fn Jz' =>
+      |> @{fold_map 6} (fn i => fn rep => fn str => fn mapx => fn Jz => fn Jz' =>
         Local_Theory.define ((dtor_bind i, NoSyn),
           (dtor_def_bind i, dtor_spec rep str mapx Jz Jz')))
         ks Rep_Ts str_finals map_FTs Jzs Jzs'
@@ -1368,7 +1370,7 @@
 
     val ((unfold_frees, (_, unfold_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> fold_map4 (fn i => fn abs => fn f => fn z =>
+      |> @{fold_map 4} (fn i => fn abs => fn f => fn z =>
         Local_Theory.define ((unfold_bind i, NoSyn), (unfold_def_bind i, unfold_spec abs f z)))
           ks Abs_Ts (map (fn i => HOLogic.mk_comp
             (mk_proj (nth lsbisAs (i - 1)), mk_beh ss i)) ks) zs
@@ -1379,7 +1381,7 @@
     val unfolds = map (Morphism.term phi) unfold_frees;
     val unfold_names = map (fst o dest_Const) unfolds;
     fun mk_unfolds passives actives =
-      map3 (fn name => fn T => fn active =>
+      @{map 3} (fn name => fn T => fn active =>
         Const (name, Library.foldr (op -->)
           (map2 (curry op -->) actives (mk_FTs (passives @ actives)), active --> T)))
       unfold_names (mk_Ts passives) actives;
@@ -1478,9 +1480,9 @@
       let
         fun mk_goal dtor ctor FT =
          mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
-        val goals = map3 mk_goal dtors ctors FTs;
+        val goals = @{map 3} mk_goal dtors ctors FTs;
       in
-        map5 (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L =>
+        @{map 5} (fn goal => fn ctor_def => fn unfold => fn map_comp_id => fn map_cong0L =>
           Goal.prove_sorry lthy [] [] goal
             (fn {context = ctxt, prems = _} => mk_dtor_o_ctor_tac ctxt ctor_def unfold map_comp_id
               map_cong0L unfold_o_dtor_thms)
@@ -1521,7 +1523,7 @@
     val corec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o corec_bind;
 
     val corec_strs =
-      map3 (fn dtor => fn sum_s => fn mapx =>
+      @{map 3} (fn dtor => fn sum_s => fn mapx =>
         mk_case_sum
           (HOLogic.mk_comp (Term.list_comb (mapx, passive_ids @ corec_Inls), dtor), sum_s))
       dtors corec_ss corec_maps;
@@ -1532,7 +1534,7 @@
 
     val ((corec_frees, (_, corec_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> fold_map3 (fn i => fn T => fn AT =>
+      |> @{fold_map 3} (fn i => fn T => fn AT =>
         Local_Theory.define ((corec_bind i, NoSyn), (corec_def_bind i, corec_spec i T AT)))
           ks Ts activeAs
       |>> apsnd split_list o split_list
@@ -1544,7 +1546,7 @@
     fun mk_corecs Ts passives actives =
       let val Tactives = map2 (curry mk_sumT) Ts actives;
       in
-        map3 (fn name => fn T => fn active =>
+        @{map 3} (fn name => fn T => fn active =>
           Const (name, Library.foldr (op -->)
             (map2 (curry op -->) actives (mk_FTs (passives @ Tactives)), active --> T)))
         corec_names Ts actives
@@ -1565,9 +1567,9 @@
           in
             mk_Trueprop_eq (lhs, rhs)
           end;
-        val goals = map5 mk_goal ks corec_ss corec_maps_rev dtors zs;
+        val goals = @{map 5} mk_goal ks corec_ss corec_maps_rev dtors zs;
       in
-        map3 (fn goal => fn unfold => fn map_cong0 =>
+        @{map 3} (fn goal => fn unfold => fn map_cong0 =>
           Goal.prove_sorry lthy [] [] goal
             (fn {context = ctxt, prems = _} => mk_corec_tac ctxt m corec_defs unfold map_cong0
               corec_Inl_sum_thms)
@@ -1611,7 +1613,7 @@
 
         fun mk_concl phi z1 z2 = HOLogic.mk_imp (phi $ z1 $ z2, HOLogic.mk_eq (z1, z2));
         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-          (map3 mk_concl phis Jzs1 Jzs2));
+          (@{map 3} mk_concl phis Jzs1 Jzs2));
 
         fun mk_rel_prem phi dtor rel Jz Jz_copy =
           let
@@ -1622,7 +1624,7 @@
               (list_all_free [Jz, Jz_copy] (HOLogic.mk_imp (phi $ Jz $ Jz_copy, concl)))
           end;
 
-        val rel_prems = map5 mk_rel_prem phis dtors rels Jzs Jzs_copy;
+        val rel_prems = @{map 5} mk_rel_prem phis dtors rels Jzs Jzs_copy;
         val dtor_coinduct_goal = Logic.list_implies (rel_prems, concl);
 
         val dtor_coinduct =
@@ -1720,14 +1722,14 @@
               end;
 
             val Suc = Term.absdummy HOLogic.natT (Term.absfree hrec'
-              (HOLogic.mk_tuple (map4 mk_Suc dtors FTs_setss Jzs Jzs')));
+              (HOLogic.mk_tuple (@{map 4} mk_Suc dtors FTs_setss Jzs Jzs')));
           in
             mk_rec_nat Zero Suc
           end;
 
         val ((col_frees, (_, col_def_frees)), (lthy, lthy_old)) =
           lthy
-          |> fold_map4 (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define
+          |> @{fold_map 4} (fn j => fn Zero => fn hrec => fn hrec' => Local_Theory.define
             ((col_bind j, NoSyn), (col_def_bind j, col_spec j Zero hrec hrec')))
             ls Zeros hrecs hrecs'
           |>> apsnd split_list o split_list
@@ -1758,7 +1760,7 @@
         val setss = map (fn i => map2 (mk_set Ts i) ls passiveAs) ks;
 
         val (Jbnf_consts, lthy) =
-          fold_map7 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn T =>
+          @{fold_map 7} (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn T =>
               fn lthy =>
             define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads)
               map_b rel_b set_bs
@@ -1766,10 +1768,10 @@
                 [Const (@{const_name undefined}, T)]), NONE) lthy)
           bs map_bs rel_bs set_bss fs_maps setss Ts lthy;
 
-        val (_, Jconsts, Jconst_defs, mk_Jconsts) = split_list4 Jbnf_consts;
-        val (_, Jsetss, Jbds_Ds, _, _) = split_list5 Jconsts;
-        val (Jmap_defs, Jset_defss, Jbd_defs, _, Jrel_defs) = split_list5 Jconst_defs;
-        val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, _) = split_list5 mk_Jconsts;
+        val (_, Jconsts, Jconst_defs, mk_Jconsts) = @{split_list 4} Jbnf_consts;
+        val (_, Jsetss, Jbds_Ds, _, _) = @{split_list 5} Jconsts;
+        val (Jmap_defs, Jset_defss, Jbd_defs, _, Jrel_defs) = @{split_list 5} Jconst_defs;
+        val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, _) = @{split_list 5} mk_Jconsts;
 
         val Jrel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Jrel_defs;
         val Jset_defs = flat Jset_defss;
@@ -1793,9 +1795,9 @@
           let
             fun mk_goal fs_Jmap map dtor dtor' = mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_Jmap),
               HOLogic.mk_comp (Term.list_comb (map, fs @ fs_Jmaps), dtor));
-            val goals = map4 mk_goal fs_Jmaps map_FTFT's dtors dtor's;
+            val goals = @{map 4} mk_goal fs_Jmaps map_FTFT's dtors dtor's;
             val maps =
-              map5 (fn goal => fn unfold => fn map_comp => fn map_cong0 => fn map_arg_cong =>
+              @{map 5} (fn goal => fn unfold => fn map_comp => fn map_cong0 => fn map_arg_cong =>
                 Goal.prove_sorry lthy [] [] goal
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
                      mk_map_tac m n map_arg_cong unfold map_comp map_cong0)
@@ -1811,7 +1813,7 @@
             fun mk_prem u map dtor dtor' =
               mk_Trueprop_eq (HOLogic.mk_comp (dtor', u),
                 HOLogic.mk_comp (Term.list_comb (map, fs @ us), dtor));
-            val prems = map4 mk_prem us map_FTFT's dtors dtor's;
+            val prems = @{map 4} mk_prem us map_FTFT's dtors dtor's;
             val goal =
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
                 (map2 (curry HOLogic.mk_eq) us fs_Jmaps));
@@ -1826,7 +1828,7 @@
         val Jmap_comp0_thms =
           let
             val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-              (map3 (fn fmap => fn gmap => fn fgmap =>
+              (@{map 3} (fn fmap => fn gmap => fn fgmap =>
                  HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap))
               fs_Jmaps gs_Jmaps fgs_Jmaps))
           in
@@ -1849,17 +1851,17 @@
                   HOLogic.mk_Trueprop (mk_leq (K2 $ x2) (K1 $ x1))));
 
             val premss = map2 (fn j => fn Ks =>
-              map4 mk_passive_prem (map (fn xs => nth xs (j - 1)) FTs_setss) dtors Jzs Ks @
-                flat (map4 (fn sets => fn s => fn x1 => fn K1 =>
-                  map3 (mk_active_prem s x1 K1) (drop m sets) Jzs_copy Ks) FTs_setss dtors Jzs Ks))
+              @{map 4} mk_passive_prem (map (fn xs => nth xs (j - 1)) FTs_setss) dtors Jzs Ks @
+                flat (@{map 4} (fn sets => fn s => fn x1 => fn K1 =>
+                  @{map 3} (mk_active_prem s x1 K1) (drop m sets) Jzs_copy Ks) FTs_setss dtors Jzs Ks))
               ls Kss;
 
             val col_minimal_thms =
               let
                 fun mk_conjunct j T i K x = mk_leq (mk_col Ts nat i j T $ x) (K $ x);
                 fun mk_concl j T Ks = list_all_free Jzs
-                  (Library.foldr1 HOLogic.mk_conj (map3 (mk_conjunct j T) ks Ks Jzs));
-                val concls = map3 mk_concl ls passiveAs Kss;
+                  (Library.foldr1 HOLogic.mk_conj (@{map 3} (mk_conjunct j T) ks Ks Jzs));
+                val concls = @{map 3} mk_concl ls passiveAs Kss;
 
                 val goals = map2 (fn prems => fn concl =>
                   Logic.list_implies (prems, HOLogic.mk_Trueprop concl)) premss concls
@@ -1867,7 +1869,7 @@
                 val ctss =
                   map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls;
               in
-                map4 (fn goal => fn cts => fn col_0s => fn col_Sucs =>
+                @{map 4} (fn goal => fn cts => fn col_0s => fn col_Sucs =>
                   Goal.prove_sorry lthy [] [] goal
                     (fn {context = ctxt, prems = _} => mk_col_minimal_tac ctxt m cts col_0s
                       col_Sucs)
@@ -1877,7 +1879,7 @@
               end;
 
             fun mk_conjunct set K x = mk_leq (set $ x) (K $ x);
-            fun mk_concl sets Ks = Library.foldr1 HOLogic.mk_conj (map3 mk_conjunct sets Ks Jzs);
+            fun mk_concl sets Ks = Library.foldr1 HOLogic.mk_conj (@{map 3} mk_conjunct sets Ks Jzs);
             val concls = map2 mk_concl Jsetss_by_range Kss;
 
             val goals = map2 (fn prems => fn concl =>
@@ -1902,14 +1904,14 @@
                 HOLogic.mk_Trueprop (mk_leq (Jset1 $ x) (Jset2 $ y)));
 
             val set_incl_Jset_goalss =
-              map4 (fn dtor => fn x => fn sets => fn Jsets =>
+              @{map 4} (fn dtor => fn x => fn sets => fn Jsets =>
                 map2 (mk_set_incl_Jset dtor x) (take m sets) Jsets)
               dtors Jzs FTs_setss Jsetss_by_bnf;
 
             (*x(k) : F(i)set(m+k) (dtor(i) y(i)) ==> J(k)set(j) x(k) <= J(i)set(j) y(i)*)
             val set_Jset_incl_Jset_goalsss =
-              map4 (fn dtori => fn yi => fn sets => fn Jsetsi =>
-                map3 (fn xk => fn set => fn Jsetsk =>
+              @{map 4} (fn dtori => fn yi => fn sets => fn Jsetsi =>
+                @{map 3} (fn xk => fn set => fn Jsetsk =>
                   map2 (mk_set_Jset_incl_Jset dtori xk yi set) Jsetsk Jsetsi)
                 Jzs_copy (drop m sets) Jsetss_by_bnf)
               dtors Jzs FTs_setss Jsetss_by_bnf;
@@ -1952,12 +1954,12 @@
 
             val cTs = map (SOME o certifyT lthy) params';
             fun mk_induct_tinst phis jsets y y' =
-              map4 (fn phi => fn jset => fn Jz => fn Jz' =>
+              @{map 4} (fn phi => fn jset => fn Jz => fn Jz' =>
                 SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
                   HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz))))))
               phis jsets Jzs Jzs';
           in
-            map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
+            @{map 6} (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
               ((set_minimal
                 |> Drule.instantiate' cTs (mk_induct_tinst phis jsets y y')
                 |> unfold_thms lthy incls) OF
@@ -1976,7 +1978,7 @@
                    (map2 (fn X => mk_UNION (X $ (dtor $ z))) act_sets sets)));
             fun mk_goals eq =
               map2 (fn i => fn sets =>
-                map4 (fn Fsets =>
+                @{map 4} (fn Fsets =>
                   mk_simp_goal eq (nth Fsets (i - 1)) (drop m Fsets) sets)
                 FTs_setss dtors Jzs sets)
               ls Jsetss_by_range;
@@ -1984,7 +1986,7 @@
             val le_goals = map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj)
               (mk_goals (uncurry mk_leq));
             val set_le_thmss = map split_conj_thm
-              (map4 (fn goal => fn Jset_minimal => fn set_Jsets => fn set_Jset_Jsetss =>
+              (@{map 4} (fn goal => fn Jset_minimal => fn set_Jsets => fn set_Jset_Jsetss =>
                 Goal.prove_sorry lthy [] [] goal
                   (K (mk_set_le_tac n Jset_minimal set_Jsets set_Jset_Jsetss))
                 |> Thm.close_derivation
@@ -1993,7 +1995,7 @@
 
             val ge_goalss = map (map HOLogic.mk_Trueprop) (mk_goals (uncurry mk_leq o swap));
             val set_ge_thmss =
-              map3 (map3 (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets =>
+              @{map 3} (@{map 3} (fn goal => fn set_incl_Jset => fn set_Jset_incl_Jsets =>
                 Goal.prove_sorry lthy [] [] goal
                   (K (mk_set_ge_tac n set_incl_Jset set_Jset_incl_Jsets))
                 |> Thm.close_derivation
@@ -2017,15 +2019,15 @@
               HOLogic.mk_eq (mk_image f $ (col $ z), col' $ (map $ z));
 
             fun mk_goal f cols cols' = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj
-              (map4 (mk_col_natural f) fs_Jmaps Jzs cols cols'));
+              (@{map 4} (mk_col_natural f) fs_Jmaps Jzs cols cols'));
 
-            val goals = map3 mk_goal fs colss colss';
+            val goals = @{map 3} mk_goal fs colss colss';
 
             val ctss =
               map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals;
 
             val thms =
-              map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
+              @{map 4} (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
                 Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
                   (fn {context = ctxt, prems = _} => mk_col_natural_tac ctxt cts rec_0s rec_Sucs
                     dtor_Jmap_thms set_mapss)
@@ -2041,7 +2043,7 @@
             fun mk_col_bd z col bd = mk_ordLeq (mk_card_of (col $ z)) bd;
 
             fun mk_goal bds cols = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj
-              (map3 mk_col_bd Jzs cols bds));
+              (@{map 3} mk_col_bd Jzs cols bds));
 
             val goals = map (mk_goal Jbds) colss;
 
@@ -2049,7 +2051,7 @@
               (map (mk_goal (replicate n sbd)) colss);
 
             val thms =
-              map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
+              @{map 5} (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
                 Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN
                     mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss)
@@ -2069,7 +2071,7 @@
               mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y)));
 
             fun mk_prems sets z =
-              Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys')
+              Library.foldr1 HOLogic.mk_conj (@{map 5} (mk_prem z) sets fs fs_copy ys ys')
 
             fun mk_map_cong0 sets z fmap gmap =
               HOLogic.mk_imp (mk_prems sets z, HOLogic.mk_eq (fmap $ z, gmap $ z));
@@ -2086,14 +2088,14 @@
               |> Term.absfree y'
               |> certify lthy;
 
-            val cphis = map9 mk_cphi
+            val cphis = @{map 9} mk_cphi
               Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy;
 
             val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_coinduct_thm;
 
             val goal =
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-                (map4 mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps));
+                (@{map 4} mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps));
 
             val thm =
               Goal.prove_sorry lthy [] [] goal
@@ -2120,9 +2122,9 @@
           let
             fun mk_goal Jz Jz' dtor dtor' Jrelphi relphi =
               mk_Trueprop_eq (Jrelphi $ Jz $ Jz', relphi $ (dtor $ Jz) $ (dtor' $ Jz'));
-            val goals = map6 mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
+            val goals = @{map 6} mk_goal Jzs Jz's dtors dtor's Jrelphis relphis;
           in
-            map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
+            @{map 12} (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
               fn dtor_map => fn dtor_sets => fn dtor_inject => fn dtor_ctor =>
               fn set_map0s => fn dtor_set_incls => fn dtor_set_set_inclss =>
               Goal.prove_sorry lthy [] [] goal
@@ -2139,7 +2141,7 @@
       val zip_ranTs = passiveABs @ prodTsTs';
       val allJphis = Jphis @ activeJphis;
       val zipFTs = mk_FTs zip_ranTs;
-      val zipTs = map3 (fn T => fn T' => fn FT => T --> T' --> FT) Ts Ts' zipFTs;
+      val zipTs = @{map 3} (fn T => fn T' => fn FT => T --> T' --> FT) Ts Ts' zipFTs;
       val zip_zTs = mk_Ts passiveABs;
       val (((zips, (abs, abs')), (zip_zs, zip_zs')), names_lthy) = names_lthy
         |> mk_Frees "zip" zipTs
@@ -2176,17 +2178,17 @@
                   HOLogic.mk_conj (HOLogic.mk_eq (map $ zipxy, dtor $ x),
                     HOLogic.mk_eq (map' $ zipxy, dtor' $ y))))))
             end;
-          val helper_prems = map9 mk_helper_prem
+          val helper_prems = @{map 9} mk_helper_prem
             activeJphis in_phis zips Jzs Jz's map_all_fsts map_all_snds dtors dtor's;
           fun mk_helper_coind_phi fst phi x alt y map zip_unfold =
             list_exists_free [if fst then y else x] (HOLogic.mk_conj (phi $ x $ y,
               HOLogic.mk_eq (alt, map $ (zip_unfold $ HOLogic.mk_prod (x, y)))))
-          val coind1_phis = map6 (mk_helper_coind_phi true)
+          val coind1_phis = @{map 6} (mk_helper_coind_phi true)
             activeJphis Jzs Jzs_copy Jz's Jmap_fsts zip_unfolds;
-          val coind2_phis = map6 (mk_helper_coind_phi false)
+          val coind2_phis = @{map 6} (mk_helper_coind_phi false)
               activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds;
           fun mk_cts zs z's phis =
-            map3 (fn z => fn z' => fn phi =>
+            @{map 3} (fn z => fn z' => fn phi =>
               SOME (certify lthy (fold_rev (Term.absfree o Term.dest_Free) [z', z] phi)))
             zs z's phis @
             map (SOME o certify lthy) (splice z's zs);
@@ -2197,10 +2199,10 @@
             HOLogic.mk_imp (coind_phi, HOLogic.mk_eq (alt, z));
           val helper_coind1_concl =
             HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-              (map3 mk_helper_coind_concl Jzs Jzs_copy coind1_phis));
+              (@{map 3} mk_helper_coind_concl Jzs Jzs_copy coind1_phis));
           val helper_coind2_concl =
             HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-              (map3 mk_helper_coind_concl Jz's Jz's_copy coind2_phis));
+              (@{map 3} mk_helper_coind_concl Jz's Jz's_copy coind2_phis));
 
           fun mk_helper_coind_thms fst concl cts =
             Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl))
@@ -2220,8 +2222,8 @@
                  HOLogic.mk_eq (z, zip_unfold $ HOLogic.mk_prod (x, y))),
               phi $ (fst $ ab) $ (snd $ ab)));
           val helper_ind_phiss =
-            map4 (fn Jphi => fn ab => fn fst => fn snd =>
-              map5 (mk_helper_ind_phi Jphi ab fst snd)
+            @{map 4} (fn Jphi => fn ab => fn fst => fn snd =>
+              @{map 5} (mk_helper_ind_phi Jphi ab fst snd)
               zip_zs activeJphis Jzs Jz's zip_unfolds)
             Jphis abs fstABs sndABs;
           val ctss = map2 (fn ab' => fn phis =>
@@ -2234,13 +2236,13 @@
             mk_Ball (set $ z) (Term.absfree ab' ind_phi);
 
           val mk_helper_ind_concls =
-            map3 (fn ab' => fn ind_phis => fn zip_sets =>
-              map3 (mk_helper_ind_concl ab') zip_zs ind_phis zip_sets)
+            @{map 3} (fn ab' => fn ind_phis => fn zip_sets =>
+              @{map 3} (mk_helper_ind_concl ab') zip_zs ind_phis zip_sets)
             abs' helper_ind_phiss zip_setss
             |> map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj);
 
           val helper_ind_thmss = if m = 0 then replicate n [] else
-            map4 (fn concl => fn j => fn set_induct => fn cts =>
+            @{map 4} (fn concl => fn j => fn set_induct => fn cts =>
               Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl))
                 (fn {context = ctxt, prems = _} => mk_rel_coinduct_ind_tac ctxt m ks
                   dtor_unfold_thms set_mapss j (cterm_instantiate_pos cts set_induct))
@@ -2262,7 +2264,7 @@
           let
             fun mk_le_Jrel_OO Jrelpsi1 Jrelpsi2 Jrelpsi12 =
               mk_leq (mk_rel_compp (Jrelpsi1, Jrelpsi2)) Jrelpsi12;
-            val goals = map3 mk_le_Jrel_OO Jrelpsi1s Jrelpsi2s Jrelpsi12s;
+            val goals = @{map 3} mk_le_Jrel_OO Jrelpsi1s Jrelpsi2s Jrelpsi12s;
 
             val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
           in
@@ -2380,9 +2382,9 @@
                     else @{term True}));
               in
                 HOLogic.mk_Trueprop
-                  (Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct sets Jzs dummys wits))
+                  (Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct sets Jzs dummys wits))
               end;
-            val goals = map5 mk_goal Jsetss_by_range ys ys_copy ys'_copy ls;
+            val goals = @{map 5} mk_goal Jsetss_by_range ys ys_copy ys'_copy ls;
           in
             map2 (fn goal => fn induct =>
               Goal.prove_sorry lthy [] [] goal
@@ -2432,14 +2434,14 @@
 
         val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Jrel_unabs_defs;
 
-        val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
+        val tacss = @{map 9} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
           bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
 
         fun wit_tac thms ctxt =
           mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms;
 
         val (Jbnfs, lthy) =
-          fold_map6 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms =>
+          @{fold_map 6} (fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms =>
               fn consts =>
             bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms)
               (SOME deads) map_b rel_b set_bs consts)
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -289,7 +289,7 @@
             val Type (_, dom_Ts) = domain_type (fastype_of1 (bound_Ts, t));
             val map' = mk_map (length fs) dom_Ts Us map0;
             val fs' =
-              map_flattened_map_args ctxt s (map3 (massage_map_or_map_arg bound_Ts) Us Ts) fs;
+              map_flattened_map_args ctxt s (@{map 3} (massage_map_or_map_arg bound_Ts) Us Ts) fs;
           in
             Term.list_comb (map', fs')
           end
@@ -325,7 +325,7 @@
                 val f'_T = typof f';
                 val arg_Ts = map typof args;
               in
-                Term.list_comb (f', map3 (massage_call bound_Ts) (binder_types f'_T) arg_Ts args)
+                Term.list_comb (f', @{map 3} (massage_call bound_Ts) (binder_types f'_T) arg_Ts args)
               end
             | NONE =>
               (case t of
@@ -394,7 +394,7 @@
 
         fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels};
       in
-        map3 mk_spec ctrs discs selss
+        @{map 3} mk_spec ctrs discs selss
         handle ListPair.UnequalLengths => not_codatatype ctxt res_T
       end)
   | _ => not_codatatype ctxt res_T);
@@ -452,7 +452,7 @@
     val (perm_f_hssss, _) = indexedddd perm_f_Tssss h';
 
     val fun_arg_hs =
-      flat (map3 flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss);
+      flat (@{map 3} flat_corec_preds_predsss_gettersss perm_p_hss perm_q_hssss perm_f_hssss);
 
     fun unpermute0 perm0_xs = permute_like_unique (op =) perm0_kks kks perm0_xs;
     fun unpermute perm_xs = permute_like_unique (op =) perm_indices indices perm_xs;
@@ -486,7 +486,7 @@
         corec_thm corec_disc corec_sels =
       let val nullary = not (can dest_funT (fastype_of ctr)) in
         {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_io,
-         calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
+         calls = @{map 3} (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
          distinct_discss = distinct_discss, collapse = collapse, corec_thm = corec_thm,
          corec_disc = corec_disc, corec_sels = corec_sels}
       end;
@@ -494,7 +494,7 @@
     fun mk_ctr_specs ({ctrs, discs, selss, discIs, sel_thmss, distinct_discsss, collapses, ...}
         : ctr_sugar) p_is q_isss f_isss f_Tsss corec_thms corec_discs corec_selss =
       let val p_ios = map SOME p_is @ [NONE] in
-        map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
+        @{map 14} mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
           distinct_discsss collapses corec_thms corec_discs corec_selss
       end;
 
@@ -509,7 +509,7 @@
        ctr_specs = mk_ctr_specs ctr_sugar p_is q_isss f_isss f_Tsss corec_thms corec_discs
          corec_selss};
   in
-    (map5 mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
+    (@{map 5} mk_spec fp_sugars p_iss q_issss f_issss f_Tssss, missing_res_Ts,
      co_induct_of common_coinduct_thms, strong_co_induct_of common_coinduct_thms,
      co_induct_of coinduct_thmss, strong_co_induct_of coinduct_thmss, coinduct_attrs_pair,
      is_some gfp_sugar_thms, lthy)
@@ -738,7 +738,7 @@
 
     val sequentials = replicate (length fun_names) false;
   in
-    fold_map2 (dissect_coeqn_ctr lthy fun_names sequentials basic_ctr_specss eqn_pos eqn0
+    @{fold_map 2} (dissect_coeqn_ctr lthy fun_names sequentials basic_ctr_specss eqn_pos eqn0
         (SOME (abstract (List.rev fun_args) rhs)))
       ctr_premss ctr_concls matchedsss
   end;
@@ -909,7 +909,7 @@
     |> map2 (fn Ts => fn t => if length Ts = 0 then t $ HOLogic.unit else t) arg_Tss
     |> map2 currys arg_Tss
     |> Syntax.check_terms lthy
-    |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
+    |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
       bs mxs
     |> rpair excludess'
   end;
@@ -981,7 +981,7 @@
     val frees = map (fst #>> Binding.name_of #> Free) fixes;
     val has_call = exists_subterm (member (op =) frees);
     val eqns_data =
-      fold_map2 (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss)
+      @{fold_map 2} (dissect_coeqn lthy has_call fun_names sequentials basic_ctr_specss)
         (tag_list 0 (map snd specs)) of_specs_opt []
       |> flat o fst;
 
@@ -1030,7 +1030,7 @@
       |> map (flat o snd);
 
     val arg_Tss = map (binder_types o snd o fst) fixes;
-    val disc_eqnss = map6 mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss
+    val disc_eqnss = @{map 6} mk_actual_disc_eqns bs arg_Tss exhaustives corec_specs sel_eqnss
       disc_eqnss';
     val (defs, excludess') =
       build_codefs lthy' bs mxs has_call arg_Tss corec_specs disc_eqnss sel_eqnss;
@@ -1045,7 +1045,7 @@
       else
         tac_opt;
 
-    val excludess'' = map3 (fn tac_opt => fn sequential => map (fn (j, goal) =>
+    val excludess'' = @{map 3} (fn tac_opt => fn sequential => map (fn (j, goal) =>
         (j, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation)
            (exclude_tac tac_opt sequential j), goal))))
       tac_opts sequentials excludess';
@@ -1072,7 +1072,7 @@
         de_facto_exhaustives disc_eqnss
       |> list_all_fun_args []
     val nchotomy_taut_thmss =
-      map5 (fn tac_opt => fn {exhaust_discs = res_exhaust_discs, ...} =>
+      @{map 5} (fn tac_opt => fn {exhaust_discs = res_exhaust_discs, ...} =>
           fn {code_rhs_opt, ...} :: _ => fn [] => K []
             | [goal] => fn true =>
               let
@@ -1121,7 +1121,7 @@
                 end)
             de_facto_exhaustives disc_eqnss
           |> list_all_fun_args ps
-          |> map3 (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K []
+          |> @{map 3} (fn disc_eqns as {fun_args, ...} :: _ => fn [] => K []
               | [nchotomy_thm] => fn [goal] =>
                 [mk_primcorec_exhaust_tac lthy ("" (* for "P" *) :: map (fst o dest_Free) fun_args)
                    (length disc_eqns) nchotomy_thm
@@ -1334,9 +1334,9 @@
               end)
           end;
 
-        val disc_alistss = map3 (map oo prove_disc) corec_specs excludessss disc_eqnss;
+        val disc_alistss = @{map 3} (map oo prove_disc) corec_specs excludessss disc_eqnss;
         val disc_alists = map (map snd o flat) disc_alistss;
-        val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss excludessss sel_eqnss;
+        val sel_alists = @{map 4} (map ooo prove_sel) corec_specs disc_eqnss excludessss sel_eqnss;
         val disc_thmss = map (map snd o sort_list_duplicates o flat) disc_alistss;
         val disc_thmsss' = map (map (map (snd o snd))) disc_alistss;
         val sel_thmss = map (map (fst o snd) o sort_list_duplicates) sel_alists;
@@ -1364,17 +1364,18 @@
               |> single
             end;
 
-        val disc_iff_thmss = map6 (flat ooo map2 oooo prove_disc_iff) corec_specs exhaust_thmss
+        val disc_iff_thmss = @{map 6} (flat ooo map2 oooo prove_disc_iff) corec_specs exhaust_thmss
           disc_thmsss' disc_eqnss disc_thmsss' disc_eqnss
           |> map sort_list_duplicates;
 
-        val ctr_alists = map6 (fn disc_alist => maps oooo prove_ctr disc_alist) disc_alists
+        val ctr_alists = @{map 6} (fn disc_alist => maps oooo prove_ctr disc_alist) disc_alists
           (map (map snd) sel_alists) corec_specs disc_eqnss sel_eqnss ctr_specss;
         val ctr_thmss' = map (map snd) ctr_alists;
         val ctr_thmss = map (map snd o order_list) ctr_alists;
 
-        val code_thmss = map6 prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_thmss'
-          ctr_specss;
+        val code_thmss =
+          @{map 6} prove_code exhaustives disc_eqnss sel_eqnss nchotomy_thmss ctr_thmss'
+            ctr_specss;
 
         val disc_iff_or_disc_thmss =
           map2 (fn [] => I | disc_iffs => K disc_iffs) disc_iff_thmss disc_thmss;
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -608,7 +608,7 @@
         else (rtac (sum_case_cong_weak RS trans) THEN'
           rtac (mk_sum_caseN n i) THEN' rtac (mk_sum_caseN n i RS trans)),
         rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
-        EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
+        EVERY' (@{map 3} (fn i' => fn to_sbd_inj => fn from_to_sbd =>
           DETERM o EVERY' [rtac trans, rtac o_apply, rtac prod_injectI, rtac conjI,
             rtac trans, rtac @{thm Shift_def},
             rtac equalityI, rtac subsetI, etac thin_rl,
@@ -783,7 +783,7 @@
   EVERY' [rtac Jset_minimal,
     REPEAT_DETERM_N n o rtac @{thm Un_upper1},
     REPEAT_DETERM_N n o
-      EVERY' (map3 (fn i => fn set_Jset => fn set_Jset_Jsets =>
+      EVERY' (@{map 3} (fn i => fn set_Jset => fn set_Jset_Jsets =>
         EVERY' [rtac subsetI, rtac @{thm UnI2}, rtac (mk_UnIN n i), etac @{thm UN_I},
           etac UnE, etac set_Jset, REPEAT_DETERM_N (n - 1) o etac UnE,
           EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_Jset_Jsets)])
@@ -1018,7 +1018,7 @@
     val snd_diag_nth = if fst then @{thm snd_diag_fst} else @{thm snd_diag_snd};
   in
     EVERY' [rtac coinduct,
-      EVERY' (map8 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s =>
+      EVERY' (@{map 8} (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s =>
           fn dtor_unfold => fn dtor_map => fn in_rel =>
         EVERY' [REPEAT_DETERM o resolve_tac [allI, impI, in_rel RS iffD2],
           REPEAT_DETERM o eresolve_tac [exE, conjE],
@@ -1050,7 +1050,7 @@
   let val n = length ks;
   in
     rtac set_induct 1 THEN
-    EVERY' (map3 (fn unfold => fn set_map0s => fn i =>
+    EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
       EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
         select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
         REPEAT_DETERM o eresolve_tac [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp],
@@ -1058,7 +1058,7 @@
         SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_map0s (j - 1)] @ split_id_unfolds)),
         rtac subset_refl])
     unfolds set_map0ss ks) 1 THEN
-    EVERY' (map3 (fn unfold => fn set_map0s => fn i =>
+    EVERY' (@{map 3} (fn unfold => fn set_map0s => fn i =>
       EVERY' (map (fn set_map0 =>
         EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
         select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -100,18 +100,18 @@
     val prod_sTs = map2 (curry op -->) prodFTs activeAs;
 
     (* terms *)
-    val mapsAsAs = map4 mk_map_of_bnf Dss Ass Ass bnfs;
-    val mapsAsBs = map4 mk_map_of_bnf Dss Ass Bss bnfs;
-    val mapsBsCs' = map4 mk_map_of_bnf Dss Bss Css' bnfs;
-    val mapsAsCs' = map4 mk_map_of_bnf Dss Ass Css' bnfs;
-    val map_fsts = map4 mk_map_of_bnf Dss (replicate n (passiveAs @ prodBsAs)) Bss bnfs;
-    val map_fsts_rev = map4 mk_map_of_bnf Dss Bss (replicate n (passiveAs @ prodBsAs)) bnfs;
-    fun mk_setss Ts = map3 mk_sets_of_bnf (map (replicate live) Dss)
+    val mapsAsAs = @{map 4} mk_map_of_bnf Dss Ass Ass bnfs;
+    val mapsAsBs = @{map 4} mk_map_of_bnf Dss Ass Bss bnfs;
+    val mapsBsCs' = @{map 4} mk_map_of_bnf Dss Bss Css' bnfs;
+    val mapsAsCs' = @{map 4} mk_map_of_bnf Dss Ass Css' bnfs;
+    val map_fsts = @{map 4} mk_map_of_bnf Dss (replicate n (passiveAs @ prodBsAs)) Bss bnfs;
+    val map_fsts_rev = @{map 4} mk_map_of_bnf Dss Bss (replicate n (passiveAs @ prodBsAs)) bnfs;
+    fun mk_setss Ts = @{map 3} mk_sets_of_bnf (map (replicate live) Dss)
       (map (replicate live) (replicate n Ts)) bnfs;
     val setssAs = mk_setss allAs;
-    val bd0s = map3 mk_bd_of_bnf Dss Ass bnfs;
+    val bd0s = @{map 3} mk_bd_of_bnf Dss Ass bnfs;
     val bds =
-      map3 (fn bd0 => fn Ds => fn bnf => mk_csum bd0
+      @{map 3} (fn bd0 => fn Ds => fn bnf => mk_csum bd0
         (mk_card_of (HOLogic.mk_UNIV
           (mk_T_of_bnf Ds (replicate live (fst (dest_relT (fastype_of bd0)))) bnf))))
       bd0s Dss bnfs;
@@ -209,7 +209,7 @@
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
-    val map_comp_id_thms = map5 mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
+    val map_comp_id_thms = @{map 5} mk_map_comp_id xFs mapsAsBs mapsBsCs' mapsAsCs' map_comps;
 
     (*forall a : set(m+1) x. f(m+1) a = a; ...; forall a : set(m+n) x. f(m+n) a = a ==>
       map id ... id f(m+1) ... f(m+n) x = x*)
@@ -217,7 +217,7 @@
       let
         fun mk_prem set f z z' = HOLogic.mk_Trueprop
           (mk_Ball (set $ x) (Term.absfree z' (HOLogic.mk_eq (f $ z, z))));
-        val prems = map4 mk_prem (drop m sets) self_fs zs zs';
+        val prems = @{map 4} mk_prem (drop m sets) self_fs zs zs';
         val goal = mk_Trueprop_eq (Term.list_comb (mapAsAs, passive_ids @ self_fs) $ x, x);
       in
         Goal.prove_sorry lthy [] [] (Logic.list_implies (prems, goal))
@@ -226,7 +226,7 @@
         |> singleton (Proof_Context.export names_lthy lthy)
       end;
 
-    val map_cong0L_thms = map5 mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
+    val map_cong0L_thms = @{map 5} mk_map_cong0L xFs mapsAsAs setssAs map_cong0s map_ids;
     val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs;
     val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs;
 
@@ -240,11 +240,11 @@
     (*forall i = 1 ... n: (\<forall>x \<in> Fi_in UNIV .. UNIV B1 ... Bn. si x \<in> Bi)*)
     val alg_spec =
       let
-        val ins = map3 mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs;
+        val ins = @{map 3} mk_in (replicate n (passive_UNIVs @ Bs)) setssAs FTsAs;
         fun mk_alg_conjunct B s X x x' =
           mk_Ball X (Term.absfree x' (HOLogic.mk_mem (s $ x, B)));
 
-        val rhs = Library.foldr1 HOLogic.mk_conj (map5 mk_alg_conjunct Bs ss ins xFs xFs')
+        val rhs = Library.foldr1 HOLogic.mk_conj (@{map 5} mk_alg_conjunct Bs ss ins xFs xFs')
       in
         fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss) rhs
       end;
@@ -273,7 +273,7 @@
         fun mk_prem x set B = HOLogic.mk_Trueprop (mk_leq (set $ x) B);
         fun mk_concl s x B = mk_Trueprop_mem (s $ x, B);
         val premss = map2 ((fn x => fn sets => map2 (mk_prem x) (drop m sets) Bs)) xFs setssAs;
-        val concls = map3 mk_concl ss xFs Bs;
+        val concls = @{map 3} mk_concl ss xFs Bs;
         val goals = map2 (fn prems => fn concl =>
           Logic.list_implies (alg_prem :: prems, concl)) premss concls;
       in
@@ -321,9 +321,9 @@
             (Term.absfree x' (HOLogic.mk_eq (f $ (s $ x), s' $
               (Term.list_comb (mapAsBs, passive_ids @ fs) $ x))));
         val rhs = HOLogic.mk_conj
-          (Library.foldr1 HOLogic.mk_conj (map5 mk_fbetw fs Bs B's zs zs'),
+          (Library.foldr1 HOLogic.mk_conj (@{map 5} mk_fbetw fs Bs B's zs zs'),
           Library.foldr1 HOLogic.mk_conj
-            (map8 mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs'))
+            (@{map 8} mk_mor setssAs mapsAsBs fs ss s's FTsAs xFs xFs'))
       in
         fold_rev (Term.absfree o Term.dest_Free) (Bs @ ss @ B's @ s's @ fs) rhs
       end;
@@ -354,7 +354,7 @@
         fun mk_elim_goal sets mapAsBs f s s' x T =
           Logic.list_implies ([prem, mk_elim_prem sets x T],
             mk_Trueprop_eq (f $ (s $ x), s' $ Term.list_comb (mapAsBs, passive_ids @ fs @ [x])));
-        val elim_goals = map7 mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs;
+        val elim_goals = @{map 7} mk_elim_goal setssAs mapsAsBs fs ss s's xFs FTsAs;
         fun prove goal = Goal.prove_sorry lthy [] [] goal (K (mk_mor_elim_tac mor_def))
           |> Thm.close_derivation
           |> singleton (Proof_Context.export names_lthy lthy);
@@ -414,7 +414,7 @@
 
     val mor_convol_thm =
       let
-        val maps = map3 (fn s => fn prod_s => fn mapx =>
+        val maps = @{map 3} (fn s => fn prod_s => fn mapx =>
           mk_convol (HOLogic.mk_comp (s, Term.list_comb (mapx, passive_ids @ fsts)), prod_s))
           s's prod_ss map_fsts;
       in
@@ -432,7 +432,7 @@
             (HOLogic.mk_comp (f, s),
             HOLogic.mk_comp (s', Term.list_comb (mapAsBs, passive_ids @ fs)));
         val lhs = mk_mor active_UNIVs ss (map HOLogic.mk_UNIV activeBs) s's fs;
-        val rhs = Library.foldr1 HOLogic.mk_conj (map4 mk_conjunct mapsAsBs fs ss s's);
+        val rhs = Library.foldr1 HOLogic.mk_conj (@{map 4} mk_conjunct mapsAsBs fs ss s's);
       in
         Goal.prove_sorry lthy [] [] (mk_Trueprop_eq (lhs, rhs))
           (K (mk_mor_UNIV_tac m morE_thms mor_def))
@@ -490,13 +490,13 @@
           fun mk_set_sbd i bd_Card_order bds =
             map (fn thm => @{thm ordLeq_ordIso_trans} OF
               [bd_Card_order RS mk_ordLeq_csum n i thm, sbd_ordIso]) bds;
-          val set_sbdss = map3 mk_set_sbd ks bd_Card_orders set_bdss;
+          val set_sbdss = @{map 3} mk_set_sbd ks bd_Card_orders set_bdss;
 
           fun mk_in_bd_sum i Co Cnz bd =
             Cnz RS ((@{thm ordLeq_ordIso_trans} OF
               [Co RS mk_ordLeq_csum n i (Co RS @{thm ordLeq_refl}), sbd_ordIso]) RS
               (bd RS @{thm ordLeq_transitive[OF _ cexp_mono2_Cnotzero[OF _ Card_order_csum]]}));
-          val in_sbds = map4 mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds;
+          val in_sbds = @{map 4} mk_in_bd_sum ks bd_Card_orders bd_Cnotzeros in_bds;
        in
          (lthy, sbd, sbd_Cinfinite, sbd_Card_order, set_sbdss, in_sbds)
        end;
@@ -573,7 +573,7 @@
           Library.foldr1 HOLogic.mk_prodT (map HOLogic.mk_setT BTs));
       in
          mk_worec suc_bd (Term.absfree Asi' (Term.absfree idx' (HOLogic.mk_tuple
-           (map4 (mk_minH_component Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks))))
+           (@{map 4} (mk_minH_component Asi idx) (mk_setss Ts) (mk_FTs Ts) ss ks))))
       end;
 
     val (min_algs_thms, min_algs_mono_thms, card_of_min_algs_thm, least_min_algs_thm) =
@@ -585,7 +585,7 @@
 
         val concl = HOLogic.mk_Trueprop
           (HOLogic.mk_eq (min_algs $ idx, HOLogic.mk_tuple
-            (map4 (mk_minH_component min_algs idx) setssAs FTsAs ss ks)));
+            (@{map 4} (mk_minH_component min_algs idx) setssAs FTsAs ss ks)));
         val goal = Logic.mk_implies (HOLogic.mk_Trueprop i_field, concl);
 
         val min_algs_thm = Goal.prove_sorry lthy [] [] goal
@@ -696,7 +696,7 @@
           |> Thm.close_derivation
           |> singleton (Proof_Context.export names_lthy lthy);
 
-        val leasts = map3 mk_least_thm min_algs Bs min_alg_defs;
+        val leasts = @{map 3} mk_least_thm min_algs Bs min_alg_defs;
 
         val incl_prem = HOLogic.mk_Trueprop (mk_alg Bs ss);
         val incl = Goal.prove_sorry lthy [] []
@@ -811,7 +811,7 @@
           mk_mor car_inits str_inits Bs ss init_fs_copy];
         fun mk_fun_eq f g x = HOLogic.mk_eq (f $ x, g $ x);
         val unique = HOLogic.mk_Trueprop
-          (Library.foldr1 HOLogic.mk_conj (map3 mk_fun_eq init_fs init_fs_copy init_xs));
+          (Library.foldr1 HOLogic.mk_conj (@{map 3} mk_fun_eq init_fs init_fs_copy init_xs));
         val cts = map (certify lthy) ss;
         val unique_mor =
           Goal.prove_sorry lthy [] [] (Logic.list_implies (prems @ mor_prems, unique))
@@ -839,7 +839,7 @@
           end;
       in
         Library.foldr1 HOLogic.mk_conj
-          (map6 mk_conjunct phis str_inits active_init_setss init_ins init_xFs init_xFs')
+          (@{map 6} mk_conjunct phis str_inits active_init_setss init_ins init_xFs init_xFs')
       end;
 
     val init_induct_thm =
@@ -858,7 +858,7 @@
 
     val ((T_names, (T_glob_infos, T_loc_infos)), lthy) =
       lthy
-      |> fold_map3 (fn b => fn mx => fn car_init =>
+      |> @{fold_map 3} (fn b => fn mx => fn car_init =>
         typedef (b, params, mx) car_init NONE
           (EVERY' [rtac iffD2, rtac @{thm ex_in_conv}, resolve_tac alg_not_empty_thms,
             rtac alg_init_thm] 1)) bs mixfixes car_inits
@@ -918,7 +918,7 @@
 
     val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> fold_map4 (fn i => fn abs => fn str => fn mapx =>
+      |> @{fold_map 4} (fn i => fn abs => fn str => fn mapx =>
         Local_Theory.define
           ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec abs str mapx)))
           ks Abs_Ts str_inits map_FT_inits
@@ -945,7 +945,7 @@
           |> Thm.close_derivation;
 
         fun mk_ct initFT str abs = Term.absdummy initFT (abs $ (str $ Bound 0))
-        val cts = map3 (certify lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
+        val cts = @{map 3} (certify lthy ooo mk_ct) init_FTs str_inits Abs_Ts;
 
         val mor_Abs =
           Goal.prove_sorry lthy [] []
@@ -979,7 +979,7 @@
     val folds = map (Morphism.term phi) fold_frees;
     val fold_names = map (fst o dest_Const) folds;
     fun mk_folds passives actives =
-      map3 (fn name => fn T => fn active =>
+      @{map 3} (fn name => fn T => fn active =>
         Const (name, Library.foldr (op -->)
           (map2 (curry op -->) (mk_FTs (passives @ actives)) actives, T --> active)))
       fold_names (mk_Ts passives) actives;
@@ -993,7 +993,7 @@
     val copy_thm =
       let
         val prems = HOLogic.mk_Trueprop (mk_alg Bs ss) ::
-          map3 (HOLogic.mk_Trueprop ooo mk_bij_betw) inv_fs B's Bs;
+          @{map 3} (HOLogic.mk_Trueprop ooo mk_bij_betw) inv_fs B's Bs;
         val concl = HOLogic.mk_Trueprop (list_exists_free s's
           (HOLogic.mk_conj (mk_alg B's s's, mk_mor B's s's Bs ss inv_fs)));
       in
@@ -1094,9 +1094,9 @@
       let
         fun mk_goal dtor ctor FT =
           mk_Trueprop_eq (HOLogic.mk_comp (dtor, ctor), HOLogic.id_const FT);
-        val goals = map3 mk_goal dtors ctors FTs;
+        val goals = @{map 3} mk_goal dtors ctors FTs;
       in
-        map5 (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_cong0L =>
+        @{map 5} (fn goal => fn dtor_def => fn foldx => fn map_comp_id => fn map_cong0L =>
           Goal.prove_sorry lthy [] [] goal
             (K (mk_dtor_o_ctor_tac dtor_def foldx map_comp_id map_cong0L ctor_o_fold_thms))
           |> Thm.close_derivation)
@@ -1136,7 +1136,7 @@
     val rec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o rec_bind;
 
     val rec_strs =
-      map3 (fn ctor => fn prod_s => fn mapx =>
+      @{map 3} (fn ctor => fn prod_s => fn mapx =>
         mk_convol (HOLogic.mk_comp (ctor, Term.list_comb (mapx, passive_ids @ rec_fsts)), prod_s))
       ctors rec_ss rec_maps;
 
@@ -1146,7 +1146,7 @@
 
     val ((rec_frees, (_, rec_def_frees)), (lthy, lthy_old)) =
       lthy
-      |> fold_map3 (fn i => fn T => fn AT =>
+      |> @{fold_map 3} (fn i => fn T => fn AT =>
         Local_Theory.define ((rec_bind i, NoSyn), (rec_def_bind i, rec_spec i T AT))) ks Ts activeAs
       |>> apsnd split_list o split_list
       ||> `Local_Theory.restore;
@@ -1157,7 +1157,7 @@
     fun mk_recs Ts passives actives =
       let val Tactives = map2 (curry HOLogic.mk_prodT) Ts actives;
       in
-        map3 (fn name => fn T => fn active =>
+        @{map 3} (fn name => fn T => fn active =>
           Const (name, Library.foldr (op -->)
             (map2 (curry op -->) (mk_FTs (passives @ Tactives)) actives, T --> active)))
         rec_names Ts actives
@@ -1177,7 +1177,7 @@
           in
             mk_Trueprop_eq (lhs, rhs)
           end;
-        val goals = map5 mk_goal ks rec_ss rec_maps_rev ctors xFs;
+        val goals = @{map 5} mk_goal ks rec_ss rec_maps_rev ctors xFs;
       in
         map2 (fn goal => fn foldx =>
           Goal.prove_sorry lthy [] [] goal
@@ -1221,13 +1221,13 @@
                 Logic.all z (Logic.mk_implies (prem, concl))
               end;
 
-            val IHs = map3 mk_IH phis (drop m sets) Izs;
+            val IHs = @{map 3} mk_IH phis (drop m sets) Izs;
             val concl = HOLogic.mk_Trueprop (phi $ (ctor $ x));
           in
             Logic.all x (Logic.list_implies (IHs, concl))
           end;
 
-        val prems = map4 mk_prem phis ctors FTs_setss xFs;
+        val prems = @{map 4} mk_prem phis ctors FTs_setss xFs;
 
         fun mk_concl phi z = phi $ z;
         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_concl phis Izs));
@@ -1261,20 +1261,20 @@
                 fold_rev Logic.all [z1, z2] (Logic.list_implies ([prem1, prem2], concl))
               end;
 
-            val IHs = map5 mk_IH phi2s (drop m sets) (drop m sets') Izs1 Izs2;
+            val IHs = @{map 5} mk_IH phi2s (drop m sets) (drop m sets') Izs1 Izs2;
             val concl = HOLogic.mk_Trueprop (phi $ (ctor $ x) $ (ctor' $ y));
           in
             fold_rev Logic.all [x, y] (Logic.list_implies (IHs, concl))
           end;
 
-        val prems = map7 mk_prem phi2s ctors ctor's FTs_setss FTs'_setss xFs yFs;
+        val prems = @{map 7} mk_prem phi2s ctors ctor's FTs_setss FTs'_setss xFs yFs;
 
         fun mk_concl phi z1 z2 = phi $ z1 $ z2;
         val concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-          (map3 mk_concl phi2s Izs1 Izs2));
+          (@{map 3} mk_concl phi2s Izs1 Izs2));
         fun mk_t phi (z1, z1') (z2, z2') =
           Term.absfree z1' (HOLogic.mk_all (fst z2', snd z2', phi $ z1 $ z2));
-        val cts = map3 (SOME o certify lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2');
+        val cts = @{map 3} (SOME o certify lthy ooo mk_t) phi2s (Izs1 ~~ Izs1') (Izs2 ~~ Izs2');
         val goal = Logic.list_implies (prems, concl);
       in
         (Goal.prove_sorry lthy [] [] goal
@@ -1347,7 +1347,7 @@
                 Library.foldl1 mk_union (map mk_UN (drop m sets))))
           end;
 
-        val colss = map5 (fn l => fn T => map3 (mk_col l T)) ls passiveAs AFss AFss' setsss;
+        val colss = @{map 5} (fn l => fn T => @{map 3} (mk_col l T)) ls passiveAs AFss AFss' setsss;
         val setss_by_range = map (fn cols => map (mk_fold Ts cols) ks) colss;
         val setss_by_bnf = transpose setss_by_range;
 
@@ -1376,7 +1376,7 @@
                 |> minimize_wits
               end;
           in
-            map3 (fn ctor => fn i => map close_wit o minimize_wits o maps (mk_wit witss ctor i))
+            @{map 3} (fn ctor => fn i => map close_wit o minimize_wits o maps (mk_wit witss ctor i))
               ctors (0 upto n - 1) witss
           end;
 
@@ -1431,23 +1431,23 @@
               fun mk_set_sbd0 i bd0_Card_order bd0s =
                 map (fn thm => @{thm ordLeq_ordIso_trans} OF
                   [bd0_Card_order RS mk_ordLeq_csum n i thm, sbd0_ordIso]) bd0s;
-              val set_sbd0ss = map3 mk_set_sbd0 ks bd0_Card_orders set_bd0ss;
+              val set_sbd0ss = @{map 3} mk_set_sbd0 ks bd0_Card_orders set_bd0ss;
             in
               (lthy, sbd0, sbd0_card_order, sbd0_Cinfinite, set_sbd0ss)
             end;
 
         val (Ibnf_consts, lthy) =
-          fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits =>
-              fn T => fn lthy =>
+          @{fold_map 8} (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
+              fn wits => fn T => fn lthy =>
             define_bnf_consts Hardly_Inline (user_policy Note_Some lthy) false (SOME deads)
               map_b rel_b set_bs
               ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd0), wits), NONE) lthy)
           bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy;
 
-        val (_, Iconsts, Iconst_defs, mk_Iconsts) = split_list4 Ibnf_consts;
-        val (_, Isetss, Ibds_Ds, Iwitss_Ds, _) = split_list5 Iconsts;
-        val (Imap_defs, Iset_defss, Ibd_defs, Iwit_defss, Irel_defs) = split_list5 Iconst_defs;
-        val (mk_Imaps_Ds, mk_It_Ds, _, mk_Irels_Ds, _) = split_list5 mk_Iconsts;
+        val (_, Iconsts, Iconst_defs, mk_Iconsts) = @{split_list 4} Ibnf_consts;
+        val (_, Isetss, Ibds_Ds, Iwitss_Ds, _) = @{split_list 5} Iconsts;
+        val (Imap_defs, Iset_defss, Ibd_defs, Iwit_defss, Irel_defs) = @{split_list 5} Iconst_defs;
+        val (mk_Imaps_Ds, mk_It_Ds, _, mk_Irels_Ds, _) = @{split_list 5} mk_Iconsts;
 
         val Irel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Irel_defs;
         val Iset_defs = flat Iset_defss;
@@ -1474,9 +1474,9 @@
             fun mk_goal fs_map map ctor ctor' =
               mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor),
                 HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_Imaps)));
-            val goals = map4 mk_goal fs_Imaps map_FTFT's ctors ctor's;
+            val goals = @{map 4} mk_goal fs_Imaps map_FTFT's ctors ctor's;
             val maps =
-              map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong0 =>
+              @{map 4} (fn goal => fn foldx => fn map_comp_id => fn map_cong0 =>
                 Goal.prove_sorry lthy [] [] goal
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
                     mk_map_tac m n foldx map_comp_id map_cong0)
@@ -1492,7 +1492,7 @@
             fun mk_prem u map ctor ctor' =
               mk_Trueprop_eq (HOLogic.mk_comp (u, ctor),
                 HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ us)));
-            val prems = map4 mk_prem us map_FTFT's ctors ctor's;
+            val prems = @{map 4} mk_prem us map_FTFT's ctors ctor's;
             val goal =
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
                 (map2 (curry HOLogic.mk_eq) us fs_Imaps));
@@ -1513,7 +1513,8 @@
               mk_Trueprop_eq (HOLogic.mk_comp (set, ctor),
                 HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets)));
             val goalss =
-              map3 (fn sets => map4 (mk_goal sets) ctors sets) Isetss_by_range colss map_setss;
+              @{map 3} (fn sets => @{map 4} (mk_goal sets) ctors sets)
+                Isetss_by_range colss map_setss;
             val setss = map (map2 (fn foldx => fn goal =>
                 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
                   unfold_thms_tac ctxt Iset_defs THEN mk_set_tac foldx)
@@ -1526,11 +1527,11 @@
                   Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets)));
             val simp_goalss =
               map2 (fn i => fn sets =>
-                map4 (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets)
+                @{map 4} (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets)
                   FTs_setss ctors xFs sets)
                 ls Isetss_by_range;
 
-            val ctor_setss = map3 (fn i => map3 (fn set_nats => fn goal => fn set =>
+            val ctor_setss = @{map 3} (fn i => @{map 3} (fn set_nats => fn goal => fn set =>
                 Goal.prove_sorry lthy [] [] goal
                   (K (mk_ctor_set_tac set (nth set_nats (i - 1)) (drop m set_nats)))
                 |> Thm.close_derivation
@@ -1563,21 +1564,21 @@
 
             val csetss = map (map (certify lthy)) Isetss_by_range';
 
-            val cphiss = map3 (fn f => fn sets => fn sets' =>
-              (map4 (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range';
+            val cphiss = @{map 3} (fn f => fn sets => fn sets' =>
+              (@{map 4} (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range';
 
             val inducts = map (fn cphis =>
               Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
 
             val goals =
-              map3 (fn f => fn sets => fn sets' =>
+              @{map 3} (fn f => fn sets => fn sets' =>
                 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-                  (map4 (mk_set_map0 f) fs_Imaps Izs sets sets')))
+                  (@{map 4} (mk_set_map0 f) fs_Imaps Izs sets sets')))
                   fs Isetss_by_range Isetss_by_range';
 
             fun mk_tac ctxt induct = mk_set_nat_tac ctxt m (rtac induct) set_mapss ctor_Imap_thms;
             val thms =
-              map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
+              @{map 5} (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
                 Goal.prove_sorry lthy [] [] goal
                   (fn {context = ctxt, prems = _} => mk_tac ctxt induct csets ctor_sets i)
                 |> Thm.close_derivation
@@ -1601,11 +1602,11 @@
             val goals =
               map (fn sets =>
                 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-                  (map3 mk_set_bd Izs Ibds sets))) Isetss_by_range;
+                  (@{map 3} mk_set_bd Izs Ibds sets))) Isetss_by_range;
 
             fun mk_tac ctxt induct = mk_set_bd_tac ctxt m (rtac induct) sbd0_Cinfinite set_sbd0ss;
             val thms =
-              map4 (fn goal => fn ctor_sets => fn induct => fn i =>
+              @{map 4} (fn goal => fn ctor_sets => fn induct => fn i =>
                 Goal.prove_sorry lthy [] [] goal
                     (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Ibd_defs THEN
                       mk_tac ctxt induct ctor_sets i)
@@ -1623,19 +1624,19 @@
 
             fun mk_map_cong0 sets z fmap gmap =
               HOLogic.mk_imp
-                (Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys'),
+                (Library.foldr1 HOLogic.mk_conj (@{map 5} (mk_prem z) sets fs fs_copy ys ys'),
                 HOLogic.mk_eq (fmap $ z, gmap $ z));
 
             fun mk_cphi sets z fmap gmap =
               certify lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap));
 
-            val cphis = map4 mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps;
+            val cphis = @{map 4} mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps;
 
             val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm;
 
             val goal =
               HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
-                (map4 mk_map_cong0 Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps));
+                (@{map 4} mk_map_cong0 Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps));
 
             val thm = Goal.prove_sorry lthy [] [] goal
                 (fn {context = ctxt, prems = _} => mk_mcong_tac ctxt (rtac induct) set_Iset_thmsss
@@ -1666,9 +1667,9 @@
           let
             fun mk_goal xF yF ctor ctor' Irelphi relphi =
               mk_Trueprop_eq (Irelphi $ (ctor $ xF) $ (ctor' $ yF), relphi $ xF $ yF);
-            val goals = map6 mk_goal xFs yFs ctors ctor's Irelphis relphis;
+            val goals = @{map 6} mk_goal xFs yFs ctors ctor's Irelphis relphis;
           in
-            map12 (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
+            @{map 12} (fn i => fn goal => fn in_rel => fn map_comp0 => fn map_cong0 =>
               fn ctor_map => fn ctor_sets => fn ctor_inject => fn ctor_dtor =>
               fn set_map0s => fn ctor_set_incls => fn ctor_set_set_inclss =>
               Goal.prove_sorry lthy [] [] goal
@@ -1686,12 +1687,12 @@
             fun mk_le_Irel_OO Irelpsi1 Irelpsi2 Irelpsi12 Iz1 Iz2 =
               HOLogic.mk_imp (mk_rel_compp (Irelpsi1, Irelpsi2) $ Iz1 $ Iz2,
                 Irelpsi12 $ Iz1 $ Iz2);
-            val goals = map5 mk_le_Irel_OO Irelpsi1s Irelpsi2s Irelpsi12s Izs1 Izs2;
+            val goals = @{map 5} mk_le_Irel_OO Irelpsi1s Irelpsi2s Irelpsi12s Izs1 Izs2;
 
             val cTs = map (SOME o certifyT lthy o TFree) induct2_params;
             val cxs = map (SOME o certify lthy) (splice Izs1 Izs2);
             fun mk_cphi z1 z2 goal = SOME (certify lthy (Term.absfree z1 (Term.absfree z2 goal)));
-            val cphis = map3 mk_cphi Izs1' Izs2' goals;
+            val cphis = @{map 3} mk_cphi Izs1' Izs2' goals;
             val induct = Drule.instantiate' cTs (cphis @ cxs) ctor_induct2_thm;
 
             val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
@@ -1720,14 +1721,14 @@
 
         val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Irel_unabs_defs;
 
-        val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
+        val tacss = @{map 9} zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
           bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
 
         fun wit_tac ctxt = unfold_thms_tac ctxt (flat Iwit_defss) THEN
           mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Ibnfs, lthy) =
-          fold_map5 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts =>
+          @{fold_map 5} (fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts =>
             bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads)
               map_b rel_b set_bs consts)
           tacss map_bs rel_bs set_bss
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -115,7 +115,7 @@
     val bs = map mk_binding b_names;
     val rhss = mk_split_rec_rhs lthy fpTs Cs recs;
   in
-    fold_map3 (define_co_rec_as Least_FP Cs) fpTs bs rhss lthy
+    @{fold_map 3} (define_co_rec_as Least_FP Cs) fpTs bs rhss lthy
   end;
 
 fun mk_split_rec_thmss ctxt Xs ctrXs_Tsss ctrss rec0_thmss (recs as rec1 :: _) rec_defs =
@@ -149,7 +149,7 @@
           (mk_Trueprop_eq (frec $ gctr, Term.list_comb (f, fgs)))
       end;
 
-    val goalss = map4 (map3 o mk_goal) frecs ctrXs_Tsss ctrss fss;
+    val goalss = @{map 4} (@{map 3} o mk_goal) frecs ctrXs_Tsss ctrss fss;
 
     fun tac ctxt =
       unfold_thms_tac ctxt (@{thms o_apply fst_conv snd_conv} @ rec_defs @ flat rec0_thmss) THEN
@@ -237,7 +237,7 @@
       (index, (T_name, map mk_dtyp Ts, map (mk_ctr_descr Ts) ctrs));
 
     val fp_ctr_sugars = map (#ctr_sugar o #fp_ctr_sugar o checked_fp_sugar_of) fpT_names;
-    val orig_descr = map3 mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars;
+    val orig_descr = @{map 3} mk_typ_descr (0 upto nn_fp - 1) fpTs fp_ctr_sugars;
     val all_infos = Old_Datatype_Data.get_all thy;
     val (orig_descr' :: nested_descrs) =
       if member (op =) prefs Keep_Nesting then [orig_descr]
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -232,7 +232,7 @@
       end;
 
     fun mk_ctr_specs fp_res_index k ctrs rec_thms =
-      map4 mk_ctr_spec ctrs (k upto k + length ctrs - 1) (nth perm_fun_arg_Tssss fp_res_index)
+      @{map 4} mk_ctr_spec ctrs (k upto k + length ctrs - 1) (nth perm_fun_arg_Tssss fp_res_index)
         rec_thms;
 
     fun mk_spec ctr_offset
@@ -433,7 +433,7 @@
     (recs, ctr_poss)
     |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos)
     |> Syntax.check_terms ctxt
-    |> map3 (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
+    |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
       bs mxs
   end;
 
@@ -595,11 +595,11 @@
     val (fixes, specs) = fst (prep_spec raw_fixes raw_specs lthy);
 
     val mk_notes =
-      flat ooo map3 (fn js => fn prefix => fn thms =>
+      flat ooo @{map 3} (fn js => fn prefix => fn thms =>
         let
           val (bs, attrss) = map_split (fst o nth specs) js;
           val notes =
-            map3 (fn b => fn attrs => fn thm =>
+            @{map 3} (fn b => fn attrs => fn thm =>
                 ((Binding.qualify false prefix b, code_nitpicksimp_simp_attrs @ attrs),
                  [([thm], [])]))
               bs attrss thms;
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -57,7 +57,7 @@
       val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs;
       val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs;
     in
-      (missing_arg_Ts, perm0_kks, map3 basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
+      (missing_arg_Ts, perm0_kks, @{map 3} basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
        fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, induct_attrs,
        is_some lfp_sugar_thms, lthy)
     end;
@@ -102,7 +102,7 @@
           let
             val Type (_, ran_Ts) = range_type (typof t);
             val map' = mk_map (length fs) Us ran_Ts map0;
-            val fs' = map_flattened_map_args ctxt s (map3 massage_map_or_map_arg Us Ts) fs;
+            val fs' = map_flattened_map_args ctxt s (@{map 3} massage_map_or_map_arg Us Ts) fs;
           in
             Term.list_comb (map', fs')
           end
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -192,7 +192,7 @@
       val nested_size_o_maps = fold (union Thm.eq_thm_prop) nested_size_o_mapss [];
 
       val ((raw_size_consts, raw_size_defs), (lthy1', lthy1)) = lthy0
-        |> apfst split_list o fold_map2 (fn b => fn rhs =>
+        |> apfst split_list o @{fold_map 2} (fn b => fn rhs =>
             Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
             #>> apsnd snd)
           size_bs size_rhss
@@ -227,7 +227,7 @@
       val (overloaded_size_defs, lthy2) = lthy1
         |> Local_Theory.background_theory_result
           (Class.instantiation (T_names, map dest_TFree As, [HOLogic.class_size])
-           #> fold_map3 define_overloaded_size overloaded_size_def_bs overloaded_size_consts
+           #> @{fold_map 3} define_overloaded_size overloaded_size_def_bs overloaded_size_consts
              overloaded_size_rhss
            ##> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
            ##> Local_Theory.exit_global);
@@ -324,7 +324,7 @@
               map2 (fold_rev (fold_rev Logic.all) [gs, hs] o HOLogic.mk_Trueprop oo
                 curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss;
             val rec_o_map_thms =
-              map3 (fn goal => fn rec_def => fn ctor_rec_o_map =>
+              @{map 3} (fn goal => fn rec_def => fn ctor_rec_o_map =>
                   Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
                     mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
                       ctor_rec_o_map)
@@ -351,7 +351,7 @@
 
             val size_o_map_thmss =
               if nested_size_o_maps_complete then
-                map3 (fn goal => fn size_def => fn rec_o_map =>
+                @{map 3} (fn goal => fn size_def => fn rec_o_map =>
                     Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
                       mk_size_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps)
                     |> Thm.close_derivation
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -473,7 +473,7 @@
       EVERY' [select_prem_tac n (dtac asm_rl) k, rtac ballI, rtac impI,
         rtac (mor_Abs RS morE RS arg_cong RS iffD2), atac,
         REPEAT_DETERM o eresolve_tac [CollectE, conjE], dtac @{thm meta_spec},
-        EVERY' (map3 mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), atac];
+        EVERY' (@{map 3} mk_IH_tac Rep_invs Abs_invs (drop m set_maps)), atac];
 
     fun mk_induct_tac (Rep, Rep_inv) =
       EVERY' [rtac (Rep_inv RS arg_cong RS iffD1), etac (Rep RSN (2, bspec))];
@@ -547,7 +547,7 @@
         REPEAT_DETERM_N (n - 1) o EVERY' (map rtac [trans, @{thm image_Un}, Un_cong]),
         EVERY' (map useIH (drop m set_nats))];
   in
-    (induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1
+    (induct_tac THEN' EVERY' (@{map 4} mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1
   end;
 
 fun mk_set_bd_tac ctxt m induct_tac bd_Cinfinite set_bdss ctor_sets i =
@@ -581,12 +581,12 @@
         EVERY' (map useIH (transpose (map tl set_setss))),
         rtac sym, rtac ctor_map];
   in
-    (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
+    (induct_tac THEN' EVERY' (@{map 3} mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
   end;
 
 fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs =
   EVERY' (rtac induct ::
-  map4 (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO =>
+  @{map 4} (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO =>
     EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}),
       REPEAT_DETERM_N 2 o dtac (Irel RS iffD1), rtac (Irel RS iffD2),
       rtac rel_mono, rtac (le_rel_OO RS @{thm predicate2D}),
@@ -725,7 +725,7 @@
   in
     unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
     EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2,
-      EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong0 =>
+      EVERY' (@{map 3} (fn IH => fn ctor_rel => fn rel_mono_strong0 =>
         EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp),
           etac rel_mono_strong0,
           REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]},
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -10,82 +10,6 @@
   include CTR_SUGAR_UTIL
   include BNF_FP_REC_SUGAR_UTIL
 
-  val map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list
-  val map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list
-  val map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i list
-  val map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
-    'i list -> 'j list
-  val map10: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
-    'i list -> 'j list -> 'k list
-  val map11: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
-    'i list -> 'j list -> 'k list -> 'l list
-  val map12: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
-    'i list -> 'j list -> 'k list -> 'l list -> 'm list
-  val map13: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
-    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list
-  val map14: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
-      'o) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
-    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list
-  val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
-      'o -> 'p) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
-    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list
-  val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
-      'o -> 'p -> 'q) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
-    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list -> 'q list
-  val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e
-  val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f -> 'g list * 'f
-  val fold_map6: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h * 'g) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g -> 'h list * 'g
-  val fold_map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i * 'h) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h -> 'i list * 'h
-  val fold_map8: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j * 'i) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i ->
-    'j list * 'i
-  val fold_map9: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k * 'j) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
-    'i list -> 'j -> 'k list * 'j
-  val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
-  val split_list5: ('a * 'b * 'c * 'd * 'e) list -> 'a list * 'b list * 'c list * 'd list * 'e list
-  val split_list6: ('a * 'b * 'c * 'd * 'e * 'f) list -> 'a list * 'b list * 'c list * 'd list *
-    'e list * 'f list
-  val split_list7: ('a * 'b * 'c * 'd * 'e * 'f * 'g) list -> 'a list * 'b list * 'c list *
-    'd list * 'e list * 'f list * 'g list
-  val split_list8: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h) list -> 'a list * 'b list * 'c list *
-    'd list * 'e list * 'f list * 'g list * 'h list
-  val split_list9: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i) list -> 'a list * 'b list *
-    'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list
-  val split_list10: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j) list -> 'a list * 'b list *
-    'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list
-  val split_list11: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k) list -> 'a list *
-    'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list *
-    'k list
-  val split_list12: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l) list -> 'a list *
-    'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list *
-    'k list * 'l list
-  val split_list13: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm) list ->
-    'a list * 'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list *
-    'j list * 'k list * 'l list * 'm list
-  val split_list14: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm * 'n) list ->
-    'a list * 'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list *
-    'j list * 'k list * 'l list * 'm list * 'n list
-  val split_list15:
-    ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm * 'n * 'o) list ->
-    'a list * 'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list *
-    'j list * 'k list * 'l list * 'm list * 'n list * 'o list
-
   val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
   val mk_Freesss: string -> typ list list list -> Proof.context ->
     term list list list * Proof.context
@@ -192,194 +116,6 @@
 
 (* Library proper *)
 
-fun map6 _ [] [] [] [] [] [] = []
-  | map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) =
-    f x1 x2 x3 x4 x5 x6 :: map6 f x1s x2s x3s x4s x5s x6s
-  | map6 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun map7 _ [] [] [] [] [] [] [] = []
-  | map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) =
-    f x1 x2 x3 x4 x5 x6 x7 :: map7 f x1s x2s x3s x4s x5s x6s x7s
-  | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun map8 _ [] [] [] [] [] [] [] [] = []
-  | map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s) =
-    f x1 x2 x3 x4 x5 x6 x7 x8 :: map8 f x1s x2s x3s x4s x5s x6s x7s x8s
-  | map8 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun map9 _ [] [] [] [] [] [] [] [] [] = []
-  | map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
-      (x9::x9s) =
-    f x1 x2 x3 x4 x5 x6 x7 x8 x9 :: map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s
-  | map9 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun map10 _ [] [] [] [] [] [] [] [] [] [] = []
-  | map10 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
-      (x9::x9s) (x10::x10s) =
-    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 :: map10 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s
-  | map10 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun map11 _ [] [] [] [] [] [] [] [] [] [] [] = []
-  | map11 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
-      (x9::x9s) (x10::x10s) (x11::x11s) =
-    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
-  | map11 _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun map12 _ [] [] [] [] [] [] [] [] [] [] [] [] = []
-  | map12 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
-      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) =
-    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ::
-      map12 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s
-  | map12 _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun map13 _ [] [] [] [] [] [] [] [] [] [] [] [] [] = []
-  | map13 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
-      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) =
-    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ::
-      map13 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s
-  | map13 _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun map14 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
-  | map14 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
-      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) =
-    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ::
-      map14 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s
-  | map14 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun map15 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
-  | map15 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
-      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) =
-    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 ::
-      map15 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s
-  | map15 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun map16 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
-  | map16 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
-      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) (x15::x15s) (x16::x16s) =
-    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 ::
-      map16 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s x16s
-  | map16 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun fold_map4 _ [] [] [] [] acc = ([], acc)
-  | fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
-    let
-      val (x, acc') = f x1 x2 x3 x4 acc;
-      val (xs, acc'') = fold_map4 f x1s x2s x3s x4s acc';
-    in (x :: xs, acc'') end
-  | fold_map4 _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun fold_map5 _ [] [] [] [] [] acc = ([], acc)
-  | fold_map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) acc =
-    let
-      val (x, acc') = f x1 x2 x3 x4 x5 acc;
-      val (xs, acc'') = fold_map5 f x1s x2s x3s x4s x5s acc';
-    in (x :: xs, acc'') end
-  | fold_map5 _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun fold_map6 _ [] [] [] [] [] [] acc = ([], acc)
-  | fold_map6 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) acc =
-    let
-      val (x, acc') = f x1 x2 x3 x4 x5 x6 acc;
-      val (xs, acc'') = fold_map6 f x1s x2s x3s x4s x5s x6s acc';
-    in (x :: xs, acc'') end
-  | fold_map6 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun fold_map7 _ [] [] [] [] [] [] [] acc = ([], acc)
-  | fold_map7 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) acc =
-    let
-      val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 acc;
-      val (xs, acc'') = fold_map7 f x1s x2s x3s x4s x5s x6s x7s acc';
-    in (x :: xs, acc'') end
-  | fold_map7 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun fold_map8 _ [] [] [] [] [] [] [] [] acc = ([], acc)
-  | fold_map8 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
-      acc =
-    let
-      val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 acc;
-      val (xs, acc'') = fold_map8 f x1s x2s x3s x4s x5s x6s x7s x8s acc';
-    in (x :: xs, acc'') end
-  | fold_map8 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun fold_map9 _ [] [] [] [] [] [] [] [] [] acc = ([], acc)
-  | fold_map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
-      (x9::x9s) acc =
-    let
-      val (x, acc') = f x1 x2 x3 x4 x5 x6 x7 x8 x9 acc;
-      val (xs, acc'') = fold_map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s acc';
-    in (x :: xs, acc'') end
-  | fold_map9 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun split_list4 [] = ([], [], [], [])
-  | split_list4 ((x1, x2, x3, x4) :: xs) =
-    let val (xs1, xs2, xs3, xs4) = split_list4 xs;
-    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
-
-fun split_list5 [] = ([], [], [], [], [])
-  | split_list5 ((x1, x2, x3, x4, x5) :: xs) =
-    let val (xs1, xs2, xs3, xs4, xs5) = split_list5 xs;
-    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5) end;
-
-fun split_list6 [] = ([], [], [], [], [], [])
-  | split_list6 ((x1, x2, x3, x4, x5, x6) :: xs) =
-    let val (xs1, xs2, xs3, xs4, xs5, xs6) = split_list6 xs;
-    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6) end;
-
-fun split_list7 [] = ([], [], [], [], [], [], [])
-  | split_list7 ((x1, x2, x3, x4, x5, x6, x7) :: xs) =
-    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7) = split_list7 xs;
-    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7) end;
-
-fun split_list8 [] = ([], [], [], [], [], [], [], [])
-  | split_list8 ((x1, x2, x3, x4, x5, x6, x7, x8) :: xs) =
-    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8) = split_list8 xs;
-    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8) end;
-
-fun split_list9 [] = ([], [], [], [], [], [], [], [], [])
-  | split_list9 ((x1, x2, x3, x4, x5, x6, x7, x8, x9) :: xs) =
-    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9) = split_list9 xs;
-    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
-        x9 :: xs9) end;
-
-fun split_list10 [] = ([], [], [], [], [], [], [], [], [], [])
-  | split_list10 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) :: xs) =
-    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10) = split_list10 xs;
-    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
-        x9 :: xs9, x10 :: xs10) end;
-
-fun split_list11 [] = ([], [], [], [], [], [], [], [], [], [], [])
-  | split_list11 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) :: xs) =
-    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11) = split_list11 xs;
-    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
-        x9 :: xs9, x10 :: xs10, x11 :: xs11) end;
-
-fun split_list12 [] = ([], [], [], [], [], [], [], [], [], [], [], [])
-  | split_list12 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) :: xs) =
-    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12) = split_list12 xs;
-    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
-        x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12) end;
-
-fun split_list13 [] = ([], [], [], [], [], [], [], [], [], [], [], [], [])
-  | split_list13 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) :: xs) =
-    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12, xs13) = split_list13 xs;
-    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
-        x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12, x13 :: xs13) end;
-
-fun split_list14 [] = ([], [], [], [], [], [], [], [], [], [], [], [], [], [])
-  | split_list14 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) :: xs) =
-    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12, xs13, xs14) =
-      split_list14 xs;
-    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
-        x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12, x13 :: xs13, x14 :: xs14) end;
-
-fun split_list15 [] = ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
-  | split_list15 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15) :: xs) =
-    let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12, xs13, xs14, xs15) =
-      split_list15 xs;
-    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
-        x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12, x13 :: xs13, x14 :: xs14, x15 :: xs15)
-    end;
-
 val parse_type_arg_constrained =
   Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
 
@@ -430,8 +166,8 @@
 
 val mk_TFreess = fold_map mk_TFrees;
 
-fun mk_Freesss x Tsss = fold_map2 mk_Freess (mk_names (length Tsss) x) Tsss;
-fun mk_Freessss x Tssss = fold_map2 mk_Freesss (mk_names (length Tssss) x) Tssss;
+fun mk_Freesss x Tsss = @{fold_map 2} mk_Freess (mk_names (length Tsss) x) Tsss;
+fun mk_Freessss x Tssss = @{fold_map 2} mk_Freesss (mk_names (length Tssss) x) Tssss;
 
 
 (** Types **)
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -414,7 +414,7 @@
 
     val disc_bindings =
       raw_disc_bindings
-      |> map4 (fn k => fn m => fn ctr => fn disc =>
+      |> @{map 4} (fn k => fn m => fn ctr => fn disc =>
         qualify false
           (if Binding.is_empty disc then
              if m = 0 then equal_binding
@@ -428,7 +428,7 @@
     fun standard_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr;
 
     val sel_bindingss =
-      map3 (fn ctr => fn m => map2 (fn l => fn sel =>
+      @{map 3} (fn ctr => fn m => map2 (fn l => fn sel =>
         qualify false
           (if Binding.is_empty sel orelse Binding.eq_name (sel, standard_binding) then
             standard_sel_binding m l ctr
@@ -476,7 +476,7 @@
 
     val case_rhs = fold_rev (fold_rev Term.lambda) [fs, [u]]
       (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $
-         Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss)));
+         Term.lambda w (Library.foldr1 HOLogic.mk_disj (@{map 3} mk_case_disj xctrs xfs xss)));
 
     val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy
       |> Local_Theory.define ((case_binding, NoSyn),
@@ -538,7 +538,7 @@
             else
               map (fn b => find_index (curry Binding.eq_name b) uniq_sel_bindings) all_sel_bindings;
 
-          val all_proto_sels = flat (map3 (fn k => fn xs => map (pair k o pair xs)) ks xss xss);
+          val all_proto_sels = flat (@{map 3} (fn k => fn xs => map (pair k o pair xs)) ks xss xss);
           val sel_infos =
             AList.group (op =) (sel_binding_index ~~ all_proto_sels)
             |> sort (int_ord o pairself fst)
@@ -565,7 +565,7 @@
             Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
 
           fun mk_sel_case_args b proto_sels T =
-            map3 (fn Const (c, _) => fn Ts => fn k =>
+            @{map 3} (fn Const (c, _) => fn Ts => fn k =>
               (case AList.lookup (op =) proto_sels k of
                 NONE =>
                 (case filter (curry (op =) (c, Binding.name_of b) o fst) sel_defaults of
@@ -596,7 +596,7 @@
 
           val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
             lthy
-            |> apfst split_list o fold_map3 (fn k => fn exist_xs_u_eq_ctr => fn b =>
+            |> apfst split_list o @{fold_map 3} (fn k => fn exist_xs_u_eq_ctr => fn b =>
                 if Binding.is_empty b then
                   if n = 1 then pair (Term.lambda u (mk_uu_eq ()), unique_disc_no_def)
                   else pair (alternate_disc k, alternate_disc_no_def)
@@ -640,7 +640,7 @@
             [fold_rev Logic.all (xs @ ys) (mk_Trueprop_eq (HOLogic.mk_eq (xctr, yctr),
               Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) xs ys)))];
       in
-        map4 mk_goal xctrs yctrs xss yss
+        @{map 4} mk_goal xctrs yctrs xss yss
       end;
 
     val half_distinct_goalss =
@@ -686,10 +686,10 @@
         val case_thms =
           let
             val goals =
-              map3 (fn xctr => fn xf => fn xs =>
+              @{map 3} (fn xctr => fn xf => fn xs =>
                 fold_rev Logic.all (fs @ xs) (mk_Trueprop_eq (fcase $ xctr, xf))) xctrs xfs xss;
           in
-            map4 (fn k => fn goal => fn injects => fn distinctss =>
+            @{map 4} (fn k => fn goal => fn injects => fn distinctss =>
                 Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
                   mk_case_tac ctxt n k case_def injects distinctss)
                 |> Thm.close_derivation)
@@ -703,7 +703,7 @@
                 mk_Trueprop_eq (xf, xg)));
 
             val goal =
-              Logic.list_implies (uv_eq :: map4 mk_prem xctrs xss xfs xgs,
+              Logic.list_implies (uv_eq :: @{map 4} mk_prem xctrs xss xfs xgs,
                  mk_Trueprop_eq (eta_ufcase, eta_vgcase));
             val weak_goal = Logic.mk_implies (uv_eq, mk_Trueprop_eq (ufcase, vfcase));
           in
@@ -723,10 +723,10 @@
 
         fun mk_split_goal xctrs xss xfs =
           mk_Trueprop_eq (split_lhs, Library.foldr1 HOLogic.mk_conj
-            (map3 mk_split_conjunct xctrs xss xfs));
+            (@{map 3} mk_split_conjunct xctrs xss xfs));
         fun mk_split_asm_goal xctrs xss xfs =
           mk_Trueprop_eq (split_lhs, HOLogic.mk_not (Library.foldr1 HOLogic.mk_disj
-            (map3 mk_split_disjunct xctrs xss xfs)));
+            (@{map 3} mk_split_disjunct xctrs xss xfs)));
 
         fun prove_split selss goal =
           Goal.prove_sorry lthy [] [] goal (fn _ =>
@@ -771,7 +771,7 @@
                 zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
                     (Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
 
-              val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
+              val sel_thmss = @{map 3} (map oo make_sel_thm) xss' case_thms sel_defss;
 
               fun has_undefined_rhs thm =
                 (case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of
@@ -833,7 +833,7 @@
                     | mk_thm _ not_discI [distinct] = distinct RS not_discI;
                   fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss;
                 in
-                  map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
+                  @{map 3} mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
                 end;
 
               val nontriv_disc_thmss =
@@ -861,7 +861,7 @@
 
                   val half_goalss = map mk_goal half_pairss;
                   val half_thmss =
-                    map3 (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
+                    @{map 3} (fn [] => K (K []) | [goal] => fn [(((m, discD), _), _)] =>
                         fn disc_thm => [prove (mk_half_distinct_disc_tac lthy m discD disc_thm) goal])
                       half_goalss half_pairss (flat disc_thmss');
 
@@ -893,9 +893,9 @@
                     in
                       (prem aconv concl, Logic.all u (Logic.mk_implies (prem, concl)))
                     end;
-                  val (trivs, goals) = map3 mk_goal ms udiscs usel_ctrs |> split_list;
+                  val (trivs, goals) = @{map 3} mk_goal ms udiscs usel_ctrs |> split_list;
                   val thms =
-                    map5 (fn m => fn discD => fn sel_thms => fn triv => fn goal =>
+                    @{map 5} (fn m => fn discD => fn sel_thms => fn triv => fn goal =>
                         Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
                           mk_collapse_tac ctxt m discD sel_thms ORELSE HEADGOAL atac)
                         |> Thm.close_derivation
@@ -933,7 +933,7 @@
 
                   val goal =
                     Library.foldr Logic.list_implies
-                      (map5 mk_prems ks udiscs uselss vdiscs vselss, uv_eq);
+                      (@{map 5} mk_prems ks udiscs uselss vdiscs vselss, uv_eq);
                   val uncollapse_thms =
                     map2 (fn thm => fn [] => thm | _ => thm RS sym) all_collapse_thms uselss;
                 in
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -100,9 +100,9 @@
   else
     let val ks = 1 upto n in
       HEADGOAL (rtac uexhaust_disc THEN'
-        EVERY' (map5 (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse =>
+        EVERY' (@{map 5} (fn k => fn m => fn distinct_discss => fn distinct_discss' => fn uuncollapse =>
           EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac, rtac sym, rtac vexhaust_disc,
-            EVERY' (map4 (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse =>
+            EVERY' (@{map 4} (fn k' => fn distinct_discs => fn distinct_discs' => fn vuncollapse =>
               EVERY'
                 (if k' = k then
                    [rtac (vuncollapse RS trans), TRY o atac] @
@@ -150,7 +150,7 @@
 
 fun mk_case_eq_if_tac ctxt n uexhaust cases discss' selss =
   HEADGOAL (rtac uexhaust THEN'
-    EVERY' (map3 (fn casex => fn if_discs => fn sels =>
+    EVERY' (@{map 3} (fn casex => fn if_discs => fn sels =>
         EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)),
           rtac casex])
       cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss));
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -10,13 +10,6 @@
 sig
   val map_prod: ('a -> 'b) -> ('c -> 'd) -> 'a * 'c -> 'b * 'd
 
-  val map3: ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
-  val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
-  val map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f) ->
-    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list
-  val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c
-  val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) ->
-    'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd
   val seq_conds: (bool -> 'a -> 'b) -> int -> int -> 'a list -> 'b list
   val transpose: 'a list list -> 'a list list
   val pad_list: 'a -> int -> 'a list -> 'a list
@@ -108,35 +101,6 @@
 
 fun map_prod f g (x, y) = (f x, g y);
 
-fun map3 _ [] [] [] = []
-  | map3 f (x1::x1s) (x2::x2s) (x3::x3s) = f x1 x2 x3 :: map3 f x1s x2s x3s
-  | map3 _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun map4 _ [] [] [] [] = []
-  | map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) = f x1 x2 x3 x4 :: map4 f x1s x2s x3s x4s
-  | map4 _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun map5 _ [] [] [] [] [] = []
-  | map5 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) =
-    f x1 x2 x3 x4 x5 :: map5 f x1s x2s x3s x4s x5s
-  | map5 _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun fold_map2 _ [] [] acc = ([], acc)
-  | fold_map2 f (x1::x1s) (x2::x2s) acc =
-    let
-      val (x, acc') = f x1 x2 acc;
-      val (xs, acc'') = fold_map2 f x1s x2s acc';
-    in (x :: xs, acc'') end
-  | fold_map2 _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun fold_map3 _ [] [] [] acc = ([], acc)
-  | fold_map3 f (x1::x1s) (x2::x2s) (x3::x3s) acc =
-    let
-      val (x, acc') = f x1 x2 x3 acc;
-      val (xs, acc'') = fold_map3 f x1s x2s x3s acc';
-    in (x :: xs, acc'') end
-  | fold_map3 _ _ _ _ _ = raise ListPair.UnequalLengths;
-
 fun seq_conds f n k xs =
   if k = n then
     map (f false) (take (k - 1) xs)
@@ -174,10 +138,10 @@
 fun mk_TFrees n = mk_TFrees' (replicate n @{sort type});
 
 fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
-fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
+fun mk_Freess' x Tss = @{fold_map 2} mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
 
 fun mk_Frees x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => map2 (curry Free) xs Ts);
-fun mk_Freess x Tss = fold_map2 mk_Frees (mk_names (length Tss) x) Tss;
+fun mk_Freess x Tss = @{fold_map 2} mk_Frees (mk_names (length Tss) x) Tss;
 
 fun dest_TFree_or_TVar (TFree sS) = sS
   | dest_TFree_or_TVar (TVar ((s, _), S)) = (s, S)
@@ -191,7 +155,7 @@
 fun variant_types ss Ss ctxt =
   let
     val (tfrees, _) =
-      fold_map2 (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt);
+      @{fold_map 2} (fn s => fn S => Name.variant s #> apfst (rpair S)) ss Ss (Variable.names_of ctxt);
     val ctxt' = fold (Variable.declare_constraints o Logic.mk_type o TFree) tfrees ctxt;
   in (tfrees, ctxt') end;
 
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -873,7 +873,7 @@
     val cert = cterm_of (Proof_Context.theory_of lthy)
 
     val xclauses = PROFILE "xclauses"
-      (map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
+      (@{map 7} (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees
         RCss GIntro_thms) RIntro_thmss
 
     val complete =
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -11,10 +11,6 @@
 
   val dest_all_all: term -> term list * term
 
-  val map4: ('a -> 'b -> 'c -> 'd -> 'e) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list
-  val map7: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) -> 'a list -> 'b list -> 'c list ->
-    'd list -> 'e list -> 'f list -> 'g list -> 'h list
-
   val unordered_pairs: 'a list -> ('a * 'a) list
 
   val rename_bound: string -> term -> term
@@ -50,14 +46,6 @@
   | dest_all_all t = ([],t)
 
 
-fun map4 f = Ctr_Sugar_Util.map4 f
-
-fun map7 _ [] [] [] [] [] [] [] = []
-  | 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
-  | map7 _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
-
-
 (* forms all "unordered pairs": [1, 2, 3] ==> [(1, 1), (1, 2), (1, 3), (2, 2), (2, 3), (3, 3)] *)
 fun unordered_pairs [] = []
   | unordered_pairs (x::xs) = map (pair x) (x::xs) @ unordered_pairs xs
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -106,7 +106,7 @@
         (MutualPart {i=i, i'=i', fvar=fvar,cargTs=caTs,f_def=def,f=NONE,f_defthm=NONE}, rew)
       end
 
-    val (parts, rews) = split_list (map4 define fs caTss resultTs (1 upto num))
+    val (parts, rews) = split_list (@{map 4} define fs caTss resultTs (1 upto num))
 
     fun convert_eqs (f, qs, gs, args, rhs) =
       let
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Lifting/lifting_bnf.ML
--- a/src/HOL/Tools/Lifting/lifting_bnf.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Lifting/lifting_bnf.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -57,7 +57,8 @@
       ||>> mk_TFrees live
       ||>> mk_TFrees (dead_of_bnf bnf)
     val argTss = map2 (fn a => fn b => [mk_pred2T a a, a --> b, b --> a,mk_pred2T a b]) As Bs
-    val ((argss, argss'), ctxt) = fold_map2 mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss) ctxt
+    val ((argss, argss'), ctxt) =
+      @{fold_map 2} mk_Frees ["R", "Abs", "Rep", "T"] (transpose argTss) ctxt
       |>> `transpose
    
     val assms = map (mk_Quotient #> HOLogic.mk_Trueprop) argss
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -1319,7 +1319,7 @@
           construct_value ctxt
               (if new_s = @{type_name prod} then @{const_name Pair}
                else @{const_name PairBox}, new_Ts ---> new_T)
-              (map3 (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
+              (@{map 3} (coerce_term hol_ctxt Ts) [new_T1, new_T2] [old_T1, old_T2]
                     [t1, t2])
         | t' => raise TERM ("Nitpick_HOL.coerce_term", [t'])
       else
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Nitpick/nitpick_kodkod.ML
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -602,7 +602,7 @@
         val old_rs = map2 (#kk_project_seq kk r) old_offsets old_arities
       in
         fold1 (#kk_product kk)
-              (map3 (rel_expr_from_rel_expr kk) Rs Rs' old_rs)
+              (@{map 3} (rel_expr_from_rel_expr kk) Rs Rs' old_rs)
       end
     else
       lone_rep_fallback kk (Struct Rs) old_R r
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -508,7 +508,7 @@
           val k2 = k div k1
         in
           list_comb (HOLogic.pair_const T1 T2,
-                     map3 (fn T => term_for_atom seen T T) [T1, T2]
+                     @{map 3} (fn T => term_for_atom seen T T) [T1, T2]
                           (* ### k2 or k1? FIXME *)
                           [j div k2, j mod k2] [k1, k2])
         end
@@ -578,7 +578,7 @@
                   if length arg_Ts = 0 then
                     []
                   else
-                    map3 (fn Ts => term_for_rep true seen Ts Ts) arg_Ts arg_Rs
+                    @{map 3} (fn Ts => term_for_rep true seen Ts Ts) arg_Ts arg_Rs
                          arg_jsss
                     |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
                     |> dest_n_tuple (length uncur_arg_Ts)
@@ -633,7 +633,7 @@
           val (js1, js2) = chop arity1 js
         in
           list_comb (HOLogic.pair_const T1 T2,
-                     map3 (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2]
+                     @{map 3} (fn T => term_for_rep true seen T T) [T1, T2] [R1, R2]
                           [[js1], [js2]])
         end
       | term_for_rep _ seen T T' (Vect (k, R')) [js] =
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -700,7 +700,7 @@
         (mk_quasi_clauses res_aa aa1 aa2))
 
 fun add_connective_frames conn mk_quasi_clauses res_frame frame1 frame2 =
-  fold I (map3 (fn (_, res_aa) => fn (_, aa1) => fn (_, aa2) =>
+  fold I (@{map 3} (fn (_, res_aa) => fn (_, aa1) => fn (_, aa2) =>
                    add_connective_var conn mk_quasi_clauses res_aa aa1 aa2)
                res_frame frame1 frame2)
 
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Nitpick/nitpick_nut.ML
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -1151,7 +1151,7 @@
                                             (j :: js, pool)
                                           end)
                                 ([], pool)
-        val ws' = map3 (fn j => fn x => fn T =>
+        val ws' = @{map 3} (fn j => fn x => fn T =>
                            constr ((1, j), T, Atom x,
                                    nick ^ " [" ^ string_of_int j ^ "]"))
                        (rev js) atom_schema type_schema
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -439,7 +439,7 @@
                 s_let Ts "l" (n + 1) dataT bool_T
                       (fn t1 =>
                           discriminate_value hol_ctxt x t1 ::
-                          map3 (sel_eq Ts x t1) (index_seq 0 n) arg_Ts args
+                          @{map 3} (sel_eq Ts x t1) (index_seq 0 n) arg_Ts args
                           |> foldr1 s_conj) t1
             else
               raise SAME ()
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Nitpick/nitpick_util.ML
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -39,7 +39,6 @@
   val all_permutations : 'a list -> 'a list list
   val chunk_list : int -> 'a list -> 'a list list
   val chunk_list_unevenly : int list -> 'a list -> 'a list list
-  val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
   val double_lookup :
     ('a * 'a -> bool) -> ('a option * 'b) list -> 'a -> 'b option
   val triple_lookup :
@@ -202,10 +201,6 @@
   | chunk_list_unevenly (k :: ks) xs =
     let val (xs1, xs2) = chop k xs in xs1 :: chunk_list_unevenly ks xs2 end
 
-fun map3 _ [] [] [] = []
-  | map3 f (x :: xs) (y :: ys) (z :: zs) = f x y z :: map3 f xs ys zs
-  | map3 _ _ _ _ = raise ListPair.UnequalLengths
-
 fun double_lookup eq ps key =
   case AList.lookup (fn (SOME x, SOME y) => eq (x, y) | _ => false) ps
                     (SOME key) of
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/SMT/smt_datatypes.ML
--- a/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_datatypes.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -38,7 +38,7 @@
 
     val selss = if has_duplicates (op aconv) (flat selss0) then [] else selss0
   in
-    Ctr_Sugar_Util.fold_map2 mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt
+    @{fold_map 2} mk_constr ctrs0 (Ctr_Sugar_Util.pad_list [] (length ctrs0) selss) ctxt
     |>> (pair T #> single)
   end
 
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -217,14 +217,14 @@
                   val time_slice = time_mult (1.0 / Real.fromInt (length labels)) (reference_time l)
                   val timeouts =
                     map (adjust_merge_timeout preplay_timeout o curry Time.+ time_slice) times0
-                  val meths_outcomess = map3 (preplay_isar_step ctxt) timeouts hopelesses succs'
+                  val meths_outcomess = @{map 3} (preplay_isar_step ctxt) timeouts hopelesses succs'
                 in
                   (case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of
                     NONE => steps
                   | SOME times =>
                     (* "l" successfully eliminated *)
                     (decrement_step_count ();
-                     map3 (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data)
+                     @{map 3} (fn time => set_preplay_outcomes_of_isar_step ctxt time preplay_data)
                        times succs' meths_outcomess;
                      map (replace_successor l labels) lfs;
                      steps_before @ update_steps succs' steps_after))
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -8,7 +8,6 @@
 sig
   val sledgehammerN : string
   val log2 : real -> real
-  val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
   val app_hd : ('a -> 'a) -> 'a list -> 'a list
   val plural_s : int -> string
   val serial_commas : string -> string list -> string list
@@ -39,8 +38,6 @@
 val log10_2 = Math.log10 2.0
 fun log2 n = Math.log10 n / log10_2
 
-fun map3 xs = Ctr_Sugar_Util.map3 xs
-
 fun app_hd f (x :: xs) = f x :: xs
 
 fun plural_s n = if n = 1 then "" else "s"
diff -r 8529745af3dc -r 9f10d82e8188 src/HOL/Tools/coinduction.ML
--- a/src/HOL/Tools/coinduction.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/HOL/Tools/coinduction.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -73,7 +73,7 @@
           val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
             |>> (fn names => Variable.variant_fixes names names_ctxt) ;
           val eqs =
-            map3 (fn name => fn T => fn (_, rhs) =>
+            @{map 3} (fn name => fn T => fn (_, rhs) =>
               HOLogic.mk_eq (Free (name, T), rhs))
             names Ts raw_eqs;
           val phi = eqs @ map (HOLogic.dest_Trueprop o prop_of) prems
diff -r 8529745af3dc -r 9f10d82e8188 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Wed Oct 08 14:34:30 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Wed Oct 08 17:09:07 2014 +0200
@@ -167,6 +167,70 @@
         in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
 
 
+(* basic combinators *)
+
+local
+
+val parameter = Parse.position Parse.nat >> (fn (n, pos) =>
+  if n > 1 then n else error ("Bad parameter: " ^ string_of_int n ^ Position.here pos));
+
+fun indices n = map string_of_int (1 upto n);
+
+fun empty n = replicate_string n " []";
+fun dummy n = replicate_string n " _";
+fun vars x n = implode (map (fn a => " " ^ x ^ a) (indices n));
+fun cons n = implode (map (fn a => " (x" ^ a ^ " :: xs" ^ a ^ ")") (indices n));
+
+val tuple = enclose "(" ")" o commas;
+fun tuple_empty n = tuple (replicate n "[]");
+fun tuple_vars x n = tuple (map (fn a => x ^ a) (indices n));
+fun tuple_cons n = "(" ^ tuple_vars "x" n ^ " :: xs)"
+fun cons_tuple n = tuple (map (fn a => "x" ^ a ^ " :: xs" ^ a) (indices n));
+
+in
+
+val _ = Theory.setup
+ (ML_Antiquotation.value @{binding map}
+    (Scan.lift parameter >> (fn n =>
+      "fn f =>\n\
+      \  let\n\
+      \    fun map _" ^ empty n ^ " = []\n\
+      \      | map f" ^ cons n ^ " = f" ^ vars "x" n ^ " :: map f" ^ vars "xs" n ^ "\n\
+      \      | map _" ^  dummy n ^ " = raise ListPair.UnequalLengths\n" ^
+      "  in map f end")) #>
+  ML_Antiquotation.value @{binding fold}
+    (Scan.lift parameter >> (fn n =>
+      "fn f =>\n\
+      \  let\n\
+      \    fun fold _" ^ empty n ^ " a = a\n\
+      \      | fold f" ^ cons n ^ " a = fold f" ^ vars "xs" n ^ " (f" ^ vars "x" n ^ " a)\n\
+      \      | fold _" ^  dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^
+      "  in fold f end")) #>
+  ML_Antiquotation.value @{binding fold_map}
+    (Scan.lift parameter >> (fn n =>
+      "fn f =>\n\
+      \  let\n\
+      \    fun fold_map _" ^ empty n ^ " a = ([], a)\n\
+      \      | fold_map f" ^ cons n ^ " a =\n\
+      \          let\n\
+      \            val (x, a') = f" ^ vars "x" n ^ " a\n\
+      \            val (xs, a'') = fold_map f" ^ vars "xs" n ^ " a'\n\
+      \          in (x :: xs, a'') end\n\
+      \      | fold_map _" ^  dummy n ^ " _ = raise ListPair.UnequalLengths\n" ^
+      "  in fold_map f end")) #>
+  ML_Antiquotation.value @{binding split_list}
+    (Scan.lift parameter >> (fn n =>
+      "fn list =>\n\
+      \  let\n\
+      \    fun split_list [] =" ^ tuple_empty n ^ "\n\
+      \      | split_list" ^ tuple_cons n ^ " =\n\
+      \          let val" ^ tuple_vars "xs" n ^ " = split_list xs\n\
+      \          in " ^ cons_tuple n ^ "end\n\
+      \  in split_list list end")))
+
+end;
+
+
 (* outer syntax *)
 
 fun with_keyword f =