
diff -r 39ba40eb2150 -r 4b6ddc5989fc src/HOL/UNITY/Comp/AllocImpl.thy
--- a/src/HOL/UNITY/Comp/AllocImpl.thy	Thu Nov 22 10:06:30 2018 +0000
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Thu Nov 22 10:06:31 2018 +0000
@@ -92,7 +92,7 @@
   merge_allowed_acts :: "('a,'b) merge_d program set"
   where "merge_allowed_acts =
        {F. AllowedActs F =
-            insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
+            insert Id (\<Union> (Acts ` preserves (funPair merge.Out iOut)))}"
 
 definition
   merge_spec :: "('a,'b) merge_d program set"




