src/HOL/UNITY/Comp/Alloc.thy

 definition
   \<comment> \<open>environmental constraints\<close>
   alloc_allowed_acts :: "'a allocState_d program set"
   where "alloc_allowed_acts =
        {F. AllowedActs F =
-            insert Id (UNION (preserves allocGiv) Acts)}"
+            insert Id (\<Union>(Acts ` (preserves allocGiv)))}"
 
 definition
   alloc_spec :: "'a allocState_d program set"
   where "alloc_spec = alloc_increasing Int alloc_safety Int alloc_progress Int
                    alloc_allowed_acts Int alloc_preserves"