clarify R2

book.tex

@@ -3346,13 +3346,14 @@ association list.
 To print the resulting value correctly, the overall type of the
 program must be threaded through the remainder of the passes. We can
 store the type within the \key{program} form as shown in Figure
-\ref{fig:type-check-R2}. The syntax for post-typechecking $R_2$
-programs as follows: \\
+\ref{fig:type-check-R2}. Let $R^\dagger_2$ be the name for the
+intermediate language produced by the type checker, which we define as
+follows: \\[1ex]
 \fbox{
 \begin{minipage}{0.87\textwidth}
 \[
 \begin{array}{lcl}
-  R_2 &::=& (\key{program}\;(\key{type}\;\itm{type})\; \Exp)
+  R^\dagger_2 &::=& (\key{program}\;(\key{type}\;\itm{type})\; \Exp)
 \end{array}
 \]
 \end{minipage}