changeset 69325 | 4b6ddc5989fc |
parent 69313 | b021008c5397 |
--- 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"