src/HOL/Wellfounded.thy
changeset 49945 fb696ff1f086
parent 48891 c0eafbd55de3
child 54295 45a5523d4a63
     1.1 --- a/src/HOL/Wellfounded.thy	Sat Oct 20 09:09:33 2012 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Sat Oct 20 09:09:34 2012 +0200
     1.3 @@ -764,9 +764,9 @@
     1.4              with Mw show "?N2 \<in> ?W" by (simp only:)
     1.5            next
     1.6              assume "M \<noteq> {}"
     1.7 -            have N2: "(?N2, M) \<in> max_ext r" 
     1.8 -              by (rule max_extI[OF _ _ `M \<noteq> {}`]) (insert asm1, auto intro: finites)
     1.9 -            
    1.10 +            from asm1 finites have N2: "(?N2, M) \<in> max_ext r" 
    1.11 +              by (rule_tac max_extI[OF _ _ `M \<noteq> {}`]) auto
    1.12 +
    1.13              with `M \<in> ?W` show "?N2 \<in> ?W" by (rule acc_downward)
    1.14            qed
    1.15            with finites have "?N1 \<union> ?N2 \<in> ?W"