Reverting changes to typing of CAUGHTadm.

Changes to this rule are now done in PR WebAssembly#244

Author: ioannad

document/core/appendix/properties.rst

@@ -670,24 +670,24 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
 
 * The :ref:`values <syntax-val>` :math:`\val^\ast` must be of type :math:`[t_0^\ast]`.
 
-* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the label :math:`(\LCATCH~[t^\ast])` prepended to the |CLABELS| vector.
+* The label type :math:`C.\CLABELS[0]` must be defined in the context.
+
+* Let :math:`C'` be the same :ref:`context <context>` as :math:`C`, but with the :ref:`label type <syntax-labeltype>` :math:`C.\CLABELS[0]` modified to :math:`(\LCATCH~[t^\ast])` in the |CLABELS| vector.
 
 * Under context :math:`C'`,
   the instruction sequence :math:`\instr^\ast` must be :ref:`valid <valid-instr-seq>` with type :math:`[] \to [t^\ast]`.
 
-* Let :math:`C''` be the same :ref:`context <context>` as :math:`C`, but with the label :math:`[t^\ast]` prepended to the |CLABELS| vector.
-
-* Then the compound instruction is valid under context :math:`C''` with type :math:`[] \to [t^\ast]`.
+* Then the compound instruction is valid under context :math:`C` with type :math:`[] \to [t^\ast]`.
 
 .. math::
    \frac{
      S \vdashexternval \EVTAG~\tagaddr : \ETTAG~[t_0^\ast]\to[]
      \qquad
      (val : t_0)^\ast
      \qquad
-     S; C,\CLABELS\,(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast]
+     S; C,\CLABELS[0]:=(\LCATCH~[t^\ast]) \vdashinstrseq \instr^\ast : [] \to [t^\ast]
    }{
-     S; C,\CLABELS\,[t^\ast] \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast]
+     S; C \vdashadmininstr \CAUGHTadm\{\tagaddr~\val^\ast\}~\instr^\ast~\END : [] \to [t^\ast]
    }