src/HOL/Tools/BNF/bnf_def_tactics.ML

     fun last_tac iffD =
       HEADGOAL (etac rel_mono_strong) THEN
       REPEAT_DETERM (HEADGOAL (etac (@{thm predicate2_transferD} RS iffD) THEN'
         REPEAT_DETERM o atac));
   in
-    REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
+    REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
     (HEADGOAL (hyp_subst_tac ctxt THEN' rtac refl) ORELSE
      REPEAT_DETERM (HEADGOAL (eresolve_tac (Tactic.make_elim (in_rel RS iffD1) ::
        @{thms exE conjE CollectE}))) THEN
      HEADGOAL (hyp_subst_tac ctxt) THEN unfold_thms_tac ctxt rel_map THEN HEADGOAL (rtac iffI) THEN
      last_tac iffD1 THEN last_tac iffD2)

       rtac CollectI THEN' CONJ_WRAP' (fn thm =>
         etac (thm RS
           @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
       set_maps;
   in
-    REPEAT_DETERM_N n (HEADGOAL (rtac @{thm rel_funI})) THEN
+    REPEAT_DETERM_N n (HEADGOAL (rtac rel_funI)) THEN
     unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
     HEADGOAL (EVERY' [rtac @{thm order_trans}, rtac rel_mono, REPEAT_DETERM_N n o atac,
       rtac @{thm predicate2I}, dtac (in_rel RS iffD1),
       REPEAT_DETERM o eresolve_tac [exE, CollectE, conjE], hyp_subst_tac ctxt,
       rtac @{thm vimage2pI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, in_tac,

   unfold_thms_tac ctxt wit_defs THEN HEADGOAL (EVERY' (map (fn thm =>
     dtac (thm RS equalityD1 RS set_mp) THEN' etac imageE THEN' atac) set_maps)) THEN ALLGOALS atac;
 
 fun mk_set_transfer_tac ctxt in_rel set_maps =
   Goal.conjunction_tac 1 THEN
-  EVERY (map (fn set_map => HEADGOAL (rtac @{thm rel_funI}) THEN
+  EVERY (map (fn set_map => HEADGOAL (rtac rel_funI) THEN
   REPEAT_DETERM (HEADGOAL (eresolve_tac (Tactic.make_elim (in_rel RS iffD1) ::
     @{thms exE conjE CollectE}))) THEN
   HEADGOAL (hyp_subst_tac ctxt THEN' rtac (@{thm iffD2[OF arg_cong2]} OF [set_map, set_map]) THEN'
     rtac @{thm rel_setI}) THEN
   REPEAT (HEADGOAL (etac imageE THEN' dtac @{thm set_mp} THEN' atac THEN'