--- a/ProgTutorial/Package/Ind_Interface.thy	Sat May 30 11:12:46 2009 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy	Sat May 30 17:40:20 2009 +0200
@@ -165,8 +165,8 @@
              OuterKeyword.thy_decl specification*}
 
 text {*
-  We call @{ML local_theory in OuterSyntax} with the kind-indicator 
-  @{ML thy_decl in OuterKeyword} since the package does not need to open 
+  We call @{ML [index] local_theory in OuterSyntax} with the kind-indicator 
+  @{ML [index] thy_decl in OuterKeyword} since the package does not need to open 
   up any proof (see Section~\ref{sec:newcommand}). 
   The auxiliary function @{text specification} in Lines 1 to 3
   gathers the information from the parser to be processed further
@@ -178,7 +178,7 @@
   eventually will be).  Also the introduction rules are just strings. What we have
   to do first is to transform the parser's output into some internal
   datastructures that can be processed further. For this we can use the
-  function @{ML read_spec in Specification}. This function takes some strings
+  function @{ML [index] read_spec in Specification}. This function takes some strings
   (with possible typing annotations) and some rule specifications, and attempts
   to find a typing according to the given type constraints given by the 
   user and the type constraints by the ``ambient'' theory. It returns