diff --git a/specifications/KeyValueStore/KVsnap.tla b/specifications/KeyValueStore/KVsnap.tla
index 1ef48f57..6b243351 100644
--- a/specifications/KeyValueStore/KVsnap.tla
+++ b/specifications/KeyValueStore/KVsnap.tla
@@ -46,7 +46,7 @@ START: \* Start the transaction
     tx := tx \union {self};
     snapshotStore := store; \* take my snapshot of store
 
-    with (rk \in SUBSET Key \ { {} }; wk \in SUBSET Key \ { {} }) {
+    with (rk \in (SUBSET Key) \ { {} }; wk \in (SUBSET Key) \ { {} }) {
         read_keys := rk;     \* select a random read-key-set  from possible read-keys
         write_keys := wk;    \* select a random write-key-set from possible write-keys  
     };
@@ -79,7 +79,7 @@ COMMIT: \* Commit the transaction to the database if there is no conflict
 }
 *)
 
-\* BEGIN TRANSLATION (chksum(pcal) = "1adfcb46" /\ chksum(tla) = "5b28617f")
+\* BEGIN TRANSLATION (chksum(pcal) = "be9e3fd6" /\ chksum(tla) = "d93ee94d")
 VARIABLES store, tx, missed, pc, snapshotStore, read_keys, write_keys, ops
 
 vars == << store, tx, missed, pc, snapshotStore, read_keys, write_keys, ops
@@ -101,8 +101,8 @@ Init == (* Global variables *)
 START(self) == /\ pc[self] = "START"
                /\ tx' = (tx \union {self})
                /\ snapshotStore' = [snapshotStore EXCEPT ![self] = store]
-               /\ \E rk \in SUBSET Key \ { {} }:
-                    \E wk \in SUBSET Key \ { {} }:
+               /\ \E rk \in (SUBSET Key) \ { {} }:
+                    \E wk \in (SUBSET Key) \ { {} }:
                       /\ read_keys' = [read_keys EXCEPT ![self] = rk]
                       /\ write_keys' = [write_keys EXCEPT ![self] = wk]
                /\ pc' = [pc EXCEPT ![self] = "READ"]
diff --git a/specifications/LevelChecking/LevelSpec.tla b/specifications/LevelChecking/LevelSpec.tla
index 6f6e6fbb..c997c870 100644
--- a/specifications/LevelChecking/LevelSpec.tla
+++ b/specifications/LevelChecking/LevelSpec.tla
@@ -983,9 +983,9 @@
                 {i \in paramNums : /\ IsOpParam(i)
                                    /\ Node[subst.subWith[i]].ref \in
                                         OpDefNodeId}
-          IN  UNION {Sub(lc) : lc \in rcd.levelConstraints}
+          IN  (UNION {Sub(lc) : lc \in rcd.levelConstraints})
                 \cup
-              UNION { {LC(i, alp) : alp \in SubALP(i)} : i \in OpDefParams },
+              (UNION { {LC(i, alp) : alp \in SubALP(i)} : i \in OpDefParams }),
 
         argLevelConstraints |->
           (******************************************************************)
@@ -1046,9 +1046,9 @@
                (* SubParamALP(i).                                           *)
                (*************************************************************)
 
-          IN  UNION {Sub(alc) : alc \in rcd.argLevelConstraints}
+          IN  (UNION {Sub(alc) : alc \in rcd.argLevelConstraints})
                 \cup
-              UNION {ALCSet(i) : i \in paramNums},
+              (UNION {ALCSet(i) : i \in paramNums}),
 
         argLevelParams |->
           (******************************************************************)
diff --git a/specifications/allocator/AllocatorImplementation.tla b/specifications/allocator/AllocatorImplementation.tla
index 87283be4..0fc6a191 100644
--- a/specifications/allocator/AllocatorImplementation.tla
+++ b/specifications/allocator/AllocatorImplementation.tla
@@ -166,11 +166,11 @@ Invariant ==  \** a lower-level invariant
   /\ \A c \in Clients : 
        /\ Cardinality(RequestsInTransit(c)) <= 1
        /\ requests[c] = unsat[c]
-                     \cup UNION RequestsInTransit(c)
-                     \cup UNION AllocsInTransit(c)
+                     \cup (UNION RequestsInTransit(c))
+                     \cup (UNION AllocsInTransit(c))
        /\ alloc[c] = holding[c] 
-                  \cup UNION AllocsInTransit(c) 
-                  \cup UNION ReturnsInTransit(c)
+                  \cup (UNION AllocsInTransit(c)) 
+                  \cup (UNION ReturnsInTransit(c))
 
 (* correctness properties in terms of clients' variables *)
 ResourceMutex ==