--- a/doc-src/Ref/syntax.tex Tue May 30 16:00:55 2000 +0200
+++ b/doc-src/Ref/syntax.tex Tue May 30 16:01:29 2000 +0200
@@ -557,15 +557,12 @@
Normalizing an \AST{} involves repeatedly applying macro rules until
none are applicable. Macro rules are chosen in order of appearance in
the theory definitions. You can watch the normalization of \AST{}s
-during parsing and printing by setting \ttindex{Syntax.trace_norm_ast}
+during parsing and printing by setting \ttindex{Syntax.trace_ast}
to {\tt true}.\index{tracing!of macros} Alternatively, use
\ttindex{Syntax.test_read}. The information displayed when tracing
includes the \AST{} before normalization ({\tt pre}), redexes with
results ({\tt rewrote}), the normal form finally reached ({\tt post})
-and some statistics ({\tt normalize}). If tracing is off,
-\ttindex{Syntax.stat_norm_ast} can be set to {\tt true} in order to
-enable printing of the normal form and statistics only.
-
+and some statistics ({\tt normalize}).
\subsection{Example: the syntax of finite sets}
\index{examples!of macros}