--- a/doc-src/IsarRef/pure.tex Tue Jan 03 11:33:18 2006 +0100
+++ b/doc-src/IsarRef/pure.tex Tue Jan 03 11:57:33 2006 +0100
@@ -797,9 +797,9 @@
\item [$\USING{\vec b}$] augments the facts being currently indicated for use
by a subsequent refinement step (such as $\APPLYNAME$ or $\PROOFNAME$).
-\item [$\UNFOLDING{\vec b}$] is structurally similar to $\USINGNAME$,
- but unfolds meta-level equations {\vec b} throughout the goal state
- and facts.
+\item [$\isarcmd{unfolding}~\vec b$] is structurally similar to
+ $\USINGNAME$, but unfolds meta-level equations $\vec b$ throughout
+ the goal state and facts.
\end{descr}