src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Wellfounded.thy	Mon Dec 28 17:43:30 2015 +0100
@@ -305,7 +305,7 @@
 lemma wf_Union: 
  "[| ALL r:R. wf r;  
      ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {}  
-  |] ==> wf(Union R)"
+  |] ==> wf (\<Union> R)"
   using wf_UN[of R "\<lambda>i. i"] by simp
 
 (*Intuition: we find an (R u S)-min element of a nonempty subset A