src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML

     val unfolds = map (fn def =>
       unfold_thms ctxt (id_apply :: vimage2p_unfolds @ abs_inverses @ no_reflexive [def])) rel_defs;
     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
         |> unfold)
       folded_C_IHs rel_monos unfolds;