SYNC;

--- a/doc-src/Ref/ref.ind	Mon Jul 20 19:06:39 1998 +0200
+++ b/doc-src/Ref/ref.ind	Tue Jul 21 08:53:24 1998 +0200
@@ -65,7 +65,7 @@
   \item {\tt APPEND}, \bold{29}, 31
   \item {\tt APPEND'}, 36
   \item {\tt Appl}, 83
-  \item {\tt aprop} nonterminal, \bold{70}
+  \item {\tt aprop} nonterminal, \bold{68}
   \item {\tt ares_tac}, \bold{20}
   \item {\tt args} nonterminal, 93
   \item {\tt Arith} theory, 118