src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/Wellfounded.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -306,7 +306,7 @@
  "[| ALL r:R. wf r;  
      ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
   |] ==> wf(Union R)"
-  using wf_UN[of R "\<lambda>i. i"] by (simp add: SUP_def)
+  using wf_UN[of R "\<lambda>i. i"] by simp
 
 (*Intuition: we find an (R u S)-min element of a nonempty subset A
              by case distinction.