[spec] Remove obsolete invoke admin instruction

Author: rossberg

document/core/appendix/properties.rst

@@ -1087,27 +1087,6 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera
    }
 
 
-.. index:: function address, extern value, extern type, function type
-
-:math:`\INVOKE~\funcaddr`
-.........................
-
-* The :ref:`external function address <syntax-externaddr>` :math:`\XAFUNC~\funcaddr` must be :ref:`valid <valid-externaddr-func>` with :ref:`external function type <syntax-externtype>` :math:`\XTFUNC~\deftype'`.
-
-* The :ref:`expansion <aux-expand-deftype>` of the :ref:`defined type <syntax-deftype>` :math:`\deftype` must be some :ref:`function type <syntax-functype>` :math:`\TFUNC~[t_1^\ast] \Tarrow [t_2^\ast])`.
-
-* Then the instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`.
-
-.. math::
-   \frac{
-     S \vdashexternaddr \XAFUNC~\funcaddr : \XTFUNC~\deftype
-     \qquad
-     \deftype \approx \TFUNC~[t_1^\ast] \Tarrow [t_2^\ast]
-   }{
-     S; C \vdashadmininstr \INVOKE~\funcaddr : [t_1^\ast] \to [t_2^\ast]
-   }
-
-
 .. index:: label, instruction, result type
 
 :math:`\LABEL_n\{\instr_0^\ast\}~\instr^\ast`

document/core/exec/instructions.rst

@@ -401,7 +401,7 @@ Furthermore, the resulting store must be :ref:`valid <valid-store>`, i.e., all d
    ~\\[-1ex]
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   S; \val^n~(\INVOKE~a) &\stepto& S'; \result
+   S; \val^n~(\REFFUNCADDR~a)~\CALLREF &\stepto& S'; \result
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
@@ -410,7 +410,7 @@ Furthermore, the resulting store must be :ref:`valid <valid-store>`, i.e., all d
      \wedge & (S'; \result) \in \X{hf}(S; \val^n) \\
      \end{array} \\
    \begin{array}{lcl@{\qquad}l}
-   S; \val^n~(\INVOKE~a) &\stepto& S; \val^n~(\INVOKE~a)
+   S; \val^n~(\REFFUNCADDR~a)~\CALLREF &\stepto& S; \val^n~(\REFFUNCADDR~a)~\CALLREF
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}

document/core/util/macros.def

@@ -1539,10 +1539,6 @@
 .. |REFEXTERN| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}extern}}
 .. |TRAP| mathdef:: \xref{exec/runtime}{syntax-trap}{\K{trap}}
 
-.. TODO remove these
-.. |INVOKE| mathdef:: \xref{exec/instructions}{exec-invoke}{\K{invoke}}
-.. |RETURNINVOKE| mathdef:: \xref{exec/instructions}{exec-invoke}{\K{return\_invoke}}
-
 
 .. Values & Results, non-terminals