diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -192,13 +192,15 @@
 
     switch e {} = {}
     switch e { default : cs } = { cs }
-    switch e { case e : cs cases } = if e { cs } else switch e { cases }
+    switch e1 { case e2 : cs cases } =
+        { if e1 = e2 { cs } else switch e1 { cases } }
 
-    x := <macro> e = disjoin(cmds); x := y
+    x := <macro> e = z := e; disjoin(cmds, z, y); x := y
     where macro.while = macro read z { cmds } write y
 
 The function `disjoin` renames the variable names in `cmds` such that there are
-no names in common with the program in which the macro call occurs.
+no names in common with the program in which the macro call occurs, except for
+the read-variable `z` and the write-variable `y`.
 
 Finally, the semantics for programs are defined as follows:
 
diff --git a/hwhile.cabal b/hwhile.cabal
--- a/hwhile.cabal
+++ b/hwhile.cabal
@@ -1,5 +1,5 @@
 name:                   hwhile
-version:                0.1.1.3
+version:                0.1.1.4
 synopsis:               An implementation of Neil D. Jones' While language
 license:                GPL-3
 license-file:           LICENSE