...

1 files changed, 2 insertions, 2 deletions

diff --git a/final.lagda b/final.lagda
index 8928ec7..4b7484a 100644
--- a/final.lagda
+++ b/final.lagda
@@ -4357,11 +4357,11 @@ Tokenisation is performed by a simple hand written lexer.
     \multicolumn{3}{@{}l}{\text{Abstracted variables.}} \\
     \mysee{abstract} & ::= & \mytermi{postulate}\ \mysee{typed} \\
     \multicolumn{3}{@{}l}{\text{Data types, and their constructors.}} \\
-    \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\
+    \mysee{data} & ::= & \mytermi{data}\ \mysee{name}\ \mytermi{:}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mytermi{\{}\ \mysee{constrs}\ \mytermi{\}} \\
     \mysee{constrs} & ::= & \mysee{typed} \\
                    &  |  & \mysee{typed}\ \mytermi{|}\ \mysee{constrs} \\
     \multicolumn{3}{@{}l}{\text{Records, and their projections.  The $\mysee{name}$ before the projections is the constructor name.}} \\
-    \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\
+    \mysee{record} & ::= & \mytermi{record}\ \mysee{name}\ \mytermi{:}\ \mysee{telescope}\ \mytermi{->}\ \mytermi{*}\ \mytermi{=>}\ \mysee{name}\ \mytermi{\{}\ \mysee{projs}\ \mytermi{\}} \\
     \mysee{projs} & ::= & \mysee{typed} \\
                    &  |  & \mysee{typed}\ \mytermi{,}\ \mysee{projs}
   \end{array}