src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Thu Sep 15 17:06:00 2011 +0200
+++ b/src/HOL/Wellfounded.thy	Thu Sep 15 12:40:08 2011 -0400
@@ -305,9 +305,7 @@
  "[| ALL r:R. wf r;  
      ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
   |] ==> wf(Union R)"
-apply (simp add: Union_def)
-apply (blast intro: wf_UN)
-done
+  using wf_UN[of R "\<lambda>i. i"] by (simp add: SUP_def)
 
 (*Intuition: we find an (R u S)-min element of a nonempty subset A
              by case distinction.