diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -99,7 +99,7 @@
   client_allowed_acts :: "'a clientState_d program set"
   where "client_allowed_acts =
        {F. AllowedActs F =
-            insert Id (UNION (preserves (funPair rel ask)) Acts)}"
+            insert Id (\<Union> (Acts ` preserves (funPair rel ask)))}"
 
 definition
   client_spec :: "'a clientState_d program set"
@@ -208,11 +208,9 @@
   \<comment> \<open>environmental constraints\<close>
   network_allowed_acts :: "'a systemState program set"
   where "network_allowed_acts =
-       {F. AllowedActs F =
-           insert Id
-            (UNION (preserves allocRel Int
-                    (INT i: lessThan Nclients. preserves(giv o sub i o client)))
-                  Acts)}"
+       {F. AllowedActs F = insert Id
+         (\<Union> (Acts ` (preserves allocRel \<inter> (\<Inter>i<Nclients.
+           preserves (giv \<circ> sub i \<circ> client)))))}"
 
 definition
   network_spec :: "'a systemState program set"