--- a/doc-src/Ref/ref.tex Mon May 08 11:13:11 2000 +0200 +++ b/doc-src/Ref/ref.tex Mon May 08 11:13:28 2000 +0200 @@ -67,5 +67,5 @@ \endgroup \include{theory-syntax} -\input{ref.ind} +\printindex \end{document}