diff --git a/document/core/util/macros.def b/document/core/util/macros.def
index 81dc94de..2427f77f 100644
--- a/document/core/util/macros.def
+++ b/document/core/util/macros.def
@@ -212,8 +212,8 @@
 .. |MVAR| mathdef:: \xref{syntax/types}{syntax-mut}{\K{var}}
 .. |MCONST| mathdef:: \xref{syntax/types}{syntax-mut}{\K{const}}
 
-.. |SET| mathdef:: \xref{syntax/types}{syntax-init}{\mathrel{\mbox{set}}}
-.. |UNSET| mathdef:: \xref{syntax/types}{syntax-init}{\mathrel{\mbox{unset}}}
+.. |SET| mathdef:: \xref{syntax/types}{syntax-init}{\K{set}}
+.. |UNSET| mathdef:: \xref{syntax/types}{syntax-init}{\K{unset}}
 
 .. |LMIN| mathdef:: \xref{syntax/types}{syntax-limits}{\K{min}}
 .. |LMAX| mathdef:: \xref{syntax/types}{syntax-limits}{\K{max}}
diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst
index 550d8957..064f44f8 100644
--- a/document/core/valid/modules.rst
+++ b/document/core/valid/modules.rst
@@ -48,11 +48,11 @@ Functions :math:`\func` are classified by :ref:`type indices <syntax-typeidx>` r
    \frac{
      C.\CTYPES[x] = [t_1^\ast] \toF [t_2^\ast]
      \qquad
-     (C \vdashlocal t : \init~t)^\ast
+     (C \vdashlocal \{\LTYPE~t\} : \init~t)^\ast
      \qquad
      C,\CLOCALS\,(\SET~t_1)^\ast~(\init~t)^\ast,\CLABELS~[t_2^\ast],\CRETURN~[t_2^\ast] \vdashexpr \expr : [t_2^\ast]
    }{
-     C \vdashfunc \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \} : x
+     C \vdashfunc \{ \FTYPE~x, \FLOCALS~\{\LTYPE~t\}^\ast, \FBODY~\expr \} : x
    }
 
 
@@ -85,14 +85,14 @@ Locals
      \qquad
      C \vdashvaltypedefaultable t \defaultable
    }{
-     C \vdashlocal \{ \LTYPE~t \} : \SET~t \ok
+     C \vdashlocal \{ \LTYPE~t \} : \SET~t
    }
 
 .. math::
    \frac{
      C \vdashvaltype t \ok
    }{
-     C \vdashlocal \{ LTYPE~t \} : \UNSET~t \ok
+     C \vdashlocal \{ \LTYPE~t \} : \UNSET~t
    }
 
 .. note::