src/ZF/Tools/datatype_package.ML

     Goal.prove_global thy1 [] []
       (Ind_Syntax.traceIt "next case equation = " thy1 (mk_case_eqn arg))
       (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
       (fn {context = ctxt, ...} => EVERY
         [rewrite_goals_tac ctxt [con_def],
-         rtac case_trans 1,
+         resolve_tac [case_trans] 1,
          REPEAT
            (resolve_tac [@{thm refl}, split_trans,
              Su.case_inl RS @{thm trans}, Su.case_inr RS @{thm trans}] 1)]);
 
   val free_iffs = map Drule.export_without_context (con_defs RL [@{thm def_swap_iff}]);

         fun prove_recursor_eqn arg =
           Goal.prove_global thy1 [] []
             (Ind_Syntax.traceIt "next recursor equation = " thy1 (mk_recursor_eqn arg))
             (*Proves a single recursor equation.*)
             (fn {context = ctxt, ...} => EVERY
-              [rtac recursor_trans 1,
+              [resolve_tac [recursor_trans] 1,
                simp_tac (put_simpset rank_ss ctxt addsimps case_eqns) 1,
                IF_UNSOLVED (simp_tac (put_simpset rank_ss ctxt addsimps tl con_defs) 1)]);
       in
          map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases)
       end