src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML

   HEADGOAL (EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k,
     REPEAT_DETERM o dtac meta_spec, etac meta_mp, atac]) (1 upto n)));
 
 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]));
 
 fun mk_half_distinct_tac ctxt ctor_inject abs_inject ctr_defs =

     HEADGOAL (rtac (ctor_dtor_corec RS trans) THEN' asm_simp_tac ss) THEN_MAYBE
     HEADGOAL (rtac refl ORELSE' rtac (@{thm unit_eq} RS arg_cong))
   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)))
     (map rtac case_splits' @ [K all_tac]) corecs discs);
 

         unfold_thms_tac ctxt (rel_pre_T_defs @ rel_eqs)
       end;
 
     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)
   end;
 

     (if exists is_def_looping ctr_defs then
        EVERY (map (fn def => HEADGOAL (subst_asm_tac ctxt NONE [def])) ctr_defs)
      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;
 
 fun mk_coinduct_same_ctr_tac ctxt rel_eqs pre_rel_def fp_abs_inverse abs_inverse dtor_ctor ctr_def

     dtor_ctor exhaust ctr_defs discss selss =
   let val ks = 1 upto n in
     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
               mk_coinduct_same_ctr_tac ctxt rel_eqs' pre_rel_def fp_abs_inverse abs_inverse
                 dtor_ctor ctr_def discs sels

   end;
 
 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));
 
 fun mk_map_disc_iff_tac ctxt ct exhaust discs maps =
   TRYALL Goal.conjunction_tac THEN

      REPEAT_DETERM o (dtac @{thm meta_mp} THEN' rtac refl) THEN' Goal.assume_rule_tac ctxt));
 
 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]
             @{thm arg_cong2} RS iffD1)) THEN'
           atac THEN' atac THEN' hyp_subst_tac ctxt THEN' dtac assm THEN'

     cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs
       abs_inverses);
 
 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)
             THEN' atac THEN' atac THEN' TRY o resolve_tac assms))) THEN
         unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @