# HG changeset patch
# User haftmann
# Date 1145889457 -7200
# Node ID a70f1b0f09cda7a6361a099bc0049f699a01f4ee
# Parent  b6eb4b4546fa9cd34b862f7b13b1673b6a056965
more precise tactics

diff -r b6eb4b4546fa -r a70f1b0f09cd src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Mon Apr 24 16:37:07 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Mon Apr 24 16:37:37 2006 +0200
@@ -311,12 +311,12 @@
     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 =