diff --git a/spec/changelog.tex b/spec/changelog.tex
index 79db8373cd353a05d9a84988f8eaafeedcfcbf1d..4f0b57acda294ed0d2ee1ea0215735f792fb0845 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -5,10 +5,13 @@ Breaking changes:
   \item Allow arbitrary extra annotations in \texttt{assume} commands.
 \end{itemize}
 
-Clarifications:
+\noindent
+Clarifications and corrected errors:
 \begin{itemize}
   \item Clarify that the \texttt{:args} annotation in \texttt{anchor} can be
         omitted if the list is empty.
+  \item Fix mistake in proof grammar.  It now uses the \texttt{context\_annotation}
+        non-terminal in the rule for the \texttt{anchor} command.
 \end{itemize}
 
 \subsection*{0.3 --- \DTMdisplaydate{2023}{02}{10}{-1}}
diff --git a/spec/doc.tex b/spec/doc.tex
index 49e333bc66ae4e01a5f2b475988badf282342f82..414fba43a9b9036175dda2df4f5bdbffce2440d3 100644
--- a/spec/doc.tex
+++ b/spec/doc.tex
@@ -695,20 +695,20 @@ An Alethe proof is a list of commands.
                         &\grOr   & \textAlethe{(step}\; \grNT{symbol}\; \grNT{clause}
                                         \; \textAlethe{:rule}\; \grNT{symbol} \\
                         &        & \quad \grNT{premises\_annotation}^{?} \\
-                        &        & \quad \grNT{context\_annotation}^{?}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
+                        &        & \quad \grNT{args\_annotation}^{?}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
                         & \grOr  & \textAlethe{(anchor :step}\; \grNT{symbol}\;
                                             \\
-                        &        & \quad \grNT{args\_annotation}^{?}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
+                        &        & \quad \grNT{context\_annotation}^{?}\;\grNT{attribute}^{*}\,\textAlethe{)} \\
                         & \grOr  & \textAlethe{(define-fun}\; \grNT{function\_def}\,\textAlethe{)} \\
  \grNT{clause}          &\grRule & \textAlethe{(cl}\; \grNT{proof\_term}^{*}\,\textAlethe{)} \\
  \grNT{proof\_term}     &\grRule & \grNT{term}\text{ extended with } \\
                         &        & \textAlethe{(choice (}\, \grNT{sorted\_var}\,\textAlethe{)}\; \grNT{proof\_term}\,\textAlethe{)}  \\
  \grNT{premises\_annotation} &\grRule & \textAlethe{:premises (}\; \grNT{symbol}^{+}\textAlethe{)} \\
  \grNT{args\_annotation}     &\grRule & \textAlethe{:args}\,\textAlethe{(}\,\grNT{step\_arg}^{+}\,\textAlethe{)}  \\
- \grNT{step\_arg}            &\grRule & \grNT{symbol} \grOr
+ \grNT{step\_arg}            &\grRule & \grNT{symbol}\;\grOr\;
                                           \textAlethe{(}\; \grNT{symbol}\; \grNT{proof\_term}\,\textAlethe{)} \\
  \grNT{context\_annotation}  &\grRule & \textAlethe{:args}\,\textAlethe{(}\,\grNT{context\_assignment}^{+}\,\textAlethe{)}  \\
- \grNT{context\_assignment}  &\grRule & \textAlethe{(}    \,\grNT{sorted\_var}\,\textAlethe{)}  \\
+ \grNT{context\_assignment}  &\grRule & \grNT{sorted\_var} \\
                              & \grOr  & \textAlethe{(:=}\, \grNT{symbol}\;\grNT{proof\_term}\,\textAlethe{)} \\
   \end{array}
   \]