--- 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 =