--- a/doc-src/IsarRef/pure.tex Tue Sep 04 17:31:18 2001 +0200
+++ b/doc-src/IsarRef/pure.tex Tue Sep 04 21:10:57 2001 +0200
@@ -761,8 +761,8 @@
Any goal statement causes some term abbreviations (such as $\Var{thesis}$,
$\dots$) to be bound automatically, see also \S\ref{sec:term-abbrev}.
-Furthermore, the local context of a (non-atomic) goal is provided via the case
-name $antecedent$\indexisarcase{antecedent}, see also \S\ref{sec:cases}.
+Furthermore, the local context of a (non-atomic) goal is provided via the
+$rule_context$\indexisarcase{rule-context} case, see also \S\ref{sec:cases}.
\medskip