From 35cb68fcf817882de1c407d210056e9a8c6e6ec4 Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Sat, 1 Jun 2024 18:37:56 +0200
Subject: [PATCH] Convert exec/types leftover

---
 document/core/exec/types.rst | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/document/core/exec/types.rst b/document/core/exec/types.rst
index 9562224111..70c07bceab 100644
--- a/document/core/exec/types.rst
+++ b/document/core/exec/types.rst
@@ -25,8 +25,5 @@ Any form of :ref:`type <syntax-type>` can be *instantiated* into a :ref:`closed
 $${definition: inst_valtype}
 $${definition-ignore: inst_reftype}
 
-.. math::
-   \insttype_{\moduleinst}(t) = t[\subst \moduleinst.\MITYPES]
-
 .. note::
    This is the runtime equivalent to :ref:`type closure <type-closure>`.