--- a/src/HOL/UNITY/Transformers.thy	Sun Jan 27 17:30:09 2019 +0100
+++ b/src/HOL/UNITY/Transformers.thy	Mon Jan 28 10:27:47 2019 +0100
@@ -383,7 +383,7 @@
 by (simp add: wens_single_finite_Suc [symmetric]) 
 
 lemma wens_single_eq_Union:
-      "wens_single act B = \<Union>range (wens_single_finite act B)" 
+      "wens_single act B = \<Union>(range (wens_single_finite act B))" 
 by (simp add: wens_single_finite_def wens_single_def, blast) 
 
 lemma wens_single_finite_eq_Union: