# HG changeset patch
# User bulwahn
# Date 1350716974 -7200
# Node ID fb696ff1f0861cf2504606cbd8b90fccbdf5e1cd
# Parent  28cd3c9ca27838e07d326067c6575e0ee7394ae1
adjusting proofs

diff -r 28cd3c9ca278 -r fb696ff1f086 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sat Oct 20 09:09:33 2012 +0200
+++ b/src/HOL/Wellfounded.thy	Sat Oct 20 09:09:34 2012 +0200
@@ -764,9 +764,9 @@
             with Mw show "?N2 \<in> ?W" by (simp only:)
           next
             assume "M \<noteq> {}"
-            have N2: "(?N2, M) \<in> max_ext r" 
-              by (rule max_extI[OF _ _ `M \<noteq> {}`]) (insert asm1, auto intro: finites)
-            
+            from asm1 finites have N2: "(?N2, M) \<in> max_ext r" 
+              by (rule_tac max_extI[OF _ _ `M \<noteq> {}`]) auto
+
             with `M \<in> ?W` show "?N2 \<in> ?W" by (rule acc_downward)
           qed
           with finites have "?N1 \<union> ?N2 \<in> ?W"