src/HOL/Tools/BNF/bnf_gfp_tactics.ML

           (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
         if n = 1 then K all_tac
         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,
             REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl,
             etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]},

 
 fun mk_set_le_tac n Jset_minimal set_Jsets set_Jset_Jsetss =
   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)])
       (1 upto n) set_Jsets set_Jset_Jsetss)] 1;
 

     val n = length ks;
     val fst_diag_nth = if fst then @{thm fst_diag_fst} else @{thm fst_diag_snd};
     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],
           select_prem_tac (length ks) (dtac @{thm spec2}) i, dtac mp, atac,
           REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,

 
 fun mk_rel_coinduct_ind_tac ctxt m ks unfolds set_map0ss j set_induct =
   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],
         hyp_subst_tac ctxt,
         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,
         REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,
         SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map0] @ split_id_unfolds)),