--- a/ProgTutorial/Package/Ind_Interface.thy	Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy	Thu Aug 20 22:30:20 2009 +0200
@@ -138,8 +138,8 @@
              OuterKeyword.thy_decl specification*}
 
 text {*
-  We call @{ML_ind [index] local_theory in OuterSyntax} with the kind-indicator 
-  @{ML_ind [index] thy_decl in OuterKeyword} since the package does not need to open 
+  We call @{ML_ind  local_theory in OuterSyntax} with the kind-indicator 
+  @{ML_ind  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
@@ -151,7 +151,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_ind [index] read_spec in Specification}. This function takes some strings
+  function @{ML_ind  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