src/HOL/Tools/datatype_codegen.ML

     val ctxt = Context.init_proof thy;
     val inject = (#inject o DatatypePackage.the_datatype thy) dtco;
     val simpset = Simplifier.context ctxt
       (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
   in
-    (TRY o ALLGOALS o resolve_tac) [HOL.eq_reflection]
+    (TRY o ALLGOALS o match_tac) [HOL.eq_reflection]
     THEN (
-      (ALLGOALS o resolve_tac) (eqTrueI :: inject)
+      (ALLGOALS o match_tac) (eqTrueI :: inject)
       ORELSE (ALLGOALS o simp_tac) simpset
     )
-    THEN (ALLGOALS o resolve_tac) [HOL.refl, Drule.reflexive_thm]
+    THEN (ALLGOALS o match_tac) [HOL.refl, Drule.reflexive_thm]
   end;
 
 fun get_datatype_spec_thms thy dtco =
   case DatatypePackage.get_datatype_spec thy dtco
    of SOME vs_cos =>