src/HOL/Tools/BNF/bnf_lfp_compat.ML

         (Binding.prefix_name rec_split_N (Binding.name b_name));
 
     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 =
   let
     val f_Ts = binder_fun_types (fastype_of rec1);

       in
         fold_rev (fold_rev Logic.all) [fs, gs]
           (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
       HEADGOAL (rtac refl);
 

     fun mk_ctr_descr Ts = mk_ctr Ts #> dest_Const ##> (binder_types #> map mk_dtyp);
     fun mk_typ_descr index (Type (T_name, Ts)) ({ctrs, ...} : ctr_sugar) =
       (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]
       else fst (Old_Datatype_Aux.unfold_datatypes lthy orig_descr all_infos orig_descr nn_fp);