src/HOL/Tools/datatype_codegen.ML
changeset 19458 a70f1b0f09cd
parent 19346 c4c003abd830
child 19599 a5c7eb37d14f
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Mon Apr 24 16:37:07 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Mon Apr 24 16:37:37 2006 +0200
     1.3 @@ -311,12 +311,12 @@
     1.4      val simpset = Simplifier.context ctxt
     1.5        (MetaSimplifier.empty_ss addsimprocs [distinct_simproc]);
     1.6    in
     1.7 -    (TRY o ALLGOALS o resolve_tac) [HOL.eq_reflection]
     1.8 +    (TRY o ALLGOALS o match_tac) [HOL.eq_reflection]
     1.9      THEN (
    1.10 -      (ALLGOALS o resolve_tac) (eqTrueI :: inject)
    1.11 +      (ALLGOALS o match_tac) (eqTrueI :: inject)
    1.12        ORELSE (ALLGOALS o simp_tac) simpset
    1.13      )
    1.14 -    THEN (ALLGOALS o resolve_tac) [HOL.refl, Drule.reflexive_thm]
    1.15 +    THEN (ALLGOALS o match_tac) [HOL.refl, Drule.reflexive_thm]
    1.16    end;
    1.17  
    1.18  fun get_datatype_spec_thms thy dtco =