--- a/ProgTutorial/FirstSteps.thy	Mon Oct 19 14:10:42 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Mon Oct 19 17:31:13 2009 +0200
@@ -714,9 +714,10 @@
   with ML-antiquotations, often just called antiquotations.\footnote{There are
   two kinds of antiquotations in Isabelle, which have very different purposes
   and infrastructures. The first kind, described in this section, are
-  \emph{ML-antiquotations}. They are used to refer to entities (like terms,
+  \emph{\index*{ML-antiquotations}}. They are used to refer to entities (like terms,
   types etc) from Isabelle's logic layer inside ML-code. The other kind of
-  antiquotations are \emph{document} antiquotations. They are used only in the
+  antiquotations are \emph{document}\index{document antiquotationa} antiquotations. 
+  They are used only in the
   text parts of Isabelle and their purpose is to print logical entities inside
   \LaTeX-documents. Document antiquotations are part of the user level and
   therefore we are not interested in them in this Tutorial, except in Appendix