changeset 13585 | db4005b40cc6 |
parent 13524 | 604d0f3622d6 |
child 13688 | a0b16d42d489 |
--- a/src/HOL/Bali/DeclConcepts.thy Thu Sep 26 10:43:43 2002 +0200 +++ b/src/HOL/Bali/DeclConcepts.thy Thu Sep 26 10:51:29 2002 +0200 @@ -2369,9 +2369,8 @@ unique (fields G C)" apply (rule ws_subcls1_induct, assumption, assumption) apply (subst fields_rec, assumption) -apply (auto intro!: unique_map_inj injI - elim!: unique_append ws_unique_fields_lemma fields_norec - ) +apply (auto intro!: unique_map_inj inj_onI + elim!: unique_append ws_unique_fields_lemma fields_norec) done