
diff -r de49d5780f57 -r 74f0a06f751f ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Thu Aug 20 14:19:39 2009 +0200
+++ b/ProgTutorial/Tactical.thy	Thu Aug 20 22:30:20 2009 +0200
@@ -56,13 +56,13 @@
   @{text xs} that will be generalised once the goal is proved (in our case
   @{text P} and @{text Q}). The @{text "tac"} is the tactic that proves the goal;
   it can make use of the local assumptions (there are none in this example). 
-  The tactics @{ML_ind [index] etac}, @{ML_ind [index] rtac} and @{ML_ind [index] atac} 
+  The tactics @{ML_ind  etac}, @{ML_ind  rtac} and @{ML_ind  atac} 
   in the code above correspond 
   roughly to @{text erule}, @{text rule} and @{text assumption}, respectively. 
-  The operator @{ML_ind [index] THEN} strings the tactics together. 
+  The operator @{ML_ind  THEN} strings the tactics together. 
 
   \begin{readmore}
-  To learn more about the function @{ML_ind [index] prove in Goal} see \isccite{sec:results}
+  To learn more about the function @{ML_ind  prove in Goal} see \isccite{sec:results}
   and the file @{ML_file "Pure/goal.ML"}.  See @{ML_file
   "Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic
   tactics and tactic combinators; see also Chapters 3 and 4 in the old
@@ -120,7 +120,7 @@
        THEN' atac)*}text_raw{*\label{tac:footacprime}*}
 
 text {* 
-  where @{ML_ind [index] THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give 
+  where @{ML_ind  THEN'} is used instead of @{ML THEN}. With @{ML foo_tac'} you can give 
   the number for the subgoal explicitly when the tactic is
   called. So in the next proof you can first discharge the second subgoal, and
   subsequently the first.
@@ -161,7 +161,7 @@
   willy-nilly; only in very grave failure situations should a tactic raise the 
   exception @{text THM}.
 
-  The simplest tactics are @{ML_ind [index] no_tac} and @{ML_ind [index] all_tac}. The first returns
+  The simplest tactics are @{ML_ind  no_tac} and @{ML_ind  all_tac}. The first returns
   the empty sequence and is defined as
 *}
 
@@ -336,7 +336,7 @@
 section {* Simple Tactics\label{sec:simpletacs} *}
 
 text {*
-  Let us start with explaining the simple tactic @{ML_ind [index] print_tac}, which is quite useful 
+  Let us start with explaining the simple tactic @{ML_ind  print_tac}, which is quite useful 
   for low-level debugging of tactics. It just prints out a message and the current 
   goal state. Unlike @{ML my_print_tac} shown earlier, it prints the goal state 
   as the user would see it.  For example, processing the proof
@@ -356,7 +356,7 @@
 
 text {*
   A simple tactic for easy discharge of any proof obligations is 
-  @{ML_ind [index] cheat_tac in SkipProof}. This tactic corresponds to
+  @{ML_ind  cheat_tac in SkipProof}. This tactic corresponds to
   the Isabelle command \isacommand{sorry} and is sometimes useful  
   during the development of tactics.
 *}
@@ -372,7 +372,7 @@
   This tactic works however only if the quick-and-dirty mode of Isabelle 
   is switched on.
 
-  Another simple tactic is the function @{ML_ind [index] atac}, which, as shown in the previous
+  Another simple tactic is the function @{ML_ind  atac}, which, as shown in the previous
   section, corresponds to the assumption command.
 *}
 
@@ -384,8 +384,8 @@
 (*<*)oops(*>*)
 
 text {*
-  Similarly, @{ML_ind [index] rtac}, @{ML_ind [index] dtac}, @{ML_ind [index] etac} and 
-  @{ML_ind [index] ftac} correspond (roughly)
+  Similarly, @{ML_ind  rtac}, @{ML_ind  dtac}, @{ML_ind  etac} and 
+  @{ML_ind  ftac} correspond (roughly)
   to @{text rule}, @{text drule}, @{text erule} and @{text frule}, 
   respectively. Each of them takes a theorem as argument and attempts to 
   apply it to a goal. Below are three self-explanatory examples.
@@ -413,7 +413,7 @@
 (*<*)oops(*>*)
 
 text {*
-  The function @{ML_ind [index] resolve_tac} is similar to @{ML_ind [index] rtac}, except that it
+  The function @{ML_ind  resolve_tac} is similar to @{ML_ind  rtac}, except that it
   expects a list of theorems as arguments. From this list it will apply the
   first applicable theorem (later theorems that are also applicable can be
   explored via the lazy sequences mechanism). Given the code
@@ -436,11 +436,11 @@
 
 text {* 
   Similar versions taking a list of theorems exist for the tactics 
-  @{ML dtac} (@{ML_ind [index] dresolve_tac}), @{ML etac} 
-  (@{ML_ind [index] eresolve_tac}) and so on.
+  @{ML dtac} (@{ML_ind  dresolve_tac}), @{ML etac} 
+  (@{ML_ind  eresolve_tac}) and so on.
 
 
-  Another simple tactic is @{ML_ind [index] cut_facts_tac}. It inserts a list of theorems
+  Another simple tactic is @{ML_ind  cut_facts_tac}. It inserts a list of theorems
   into the assumptions of the current goal state. For example
 *}
 
@@ -475,7 +475,7 @@
   should be, then this situation can be avoided by introducing a more
   constrained version of the @{text bspec}-rule. Such constraints can be given by
   pre-instantiating theorems with other theorems. One function to do this is
-  @{ML_ind [index] "RS"}
+  @{ML_ind "RS"}
   
   @{ML_response_fake [display,gray]
   "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
@@ -489,7 +489,7 @@
 "*** Exception- THM (\"RSN: no unifiers\", 1, 
 [\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
 
-  then the function raises an exception. The function @{ML_ind [index] RSN} is similar to @{ML RS}, but 
+  then the function raises an exception. The function @{ML_ind  RSN} is similar to @{ML RS}, but 
   takes an additional number as argument that makes explicit which premise 
   should be instantiated. 
 
@@ -502,14 +502,14 @@
   "no_vars @{context} (@{thm disjI1} RS @{thm conjI})" "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> Q"}
 
   If you want to instantiate more than one premise of a theorem, you can use 
-  the function @{ML_ind [index] MRS}:
+  the function @{ML_ind  MRS}:
 
   @{ML_response_fake [display,gray]
   "no_vars @{context} ([@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI})" 
   "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> (P \<or> Qa) \<and> (Pa \<or> Q)"}
 
   If you need to instantiate lists of theorems, you can use the
-  functions @{ML RL} and @{ML_ind [index] MRL}. For example in the code below,
+  functions @{ML RL} and @{ML_ind  MRL}. For example in the code below,
   every theorem in the second list is instantiated with every 
   theorem in the first.
 
@@ -528,8 +528,8 @@
   Often proofs on the ML-level involve elaborate operations on assumptions and 
   @{text "\<And>"}-quantified variables. To do such operations using the basic tactics 
   shown so far is very unwieldy and brittle. Some convenience and
-  safety is provided by the functions @{ML_ind [index] FOCUS in Subgoal} and 
-  @{ML_ind [index] SUBPROOF}. These tactics fix the parameters 
+  safety is provided by the functions @{ML_ind  FOCUS in Subgoal} and 
+  @{ML_ind  SUBPROOF}. These tactics fix the parameters 
   and bind the various components of a goal state to a record. 
   To see what happens, use the function defined in Figure~\ref{fig:sptac}, which
   takes a record and just prints out the contents of this record. Consider
@@ -668,7 +668,7 @@
 
   Similar but less powerful functions than @{ML FOCUS in Subgoal}, respectively
   @{ML SUBPROOF}, are 
-  @{ML_ind [index] SUBGOAL} and @{ML_ind [index] CSUBGOAL}. They allow you to 
+  @{ML_ind  SUBGOAL} and @{ML_ind  CSUBGOAL}. They allow you to 
   inspect a given subgoal (the former
   presents the subgoal as a @{ML_type term}, while the latter as a @{ML_type
   cterm}). With this you can implement a tactic that applies a rule according
@@ -780,7 +780,7 @@
   in what follows we will usually prefer it over the ``unprimed'' one. 
 
   If there is a list of tactics that should all be tried out in 
-  sequence, you can use the combinator @{ML_ind [index] EVERY'}. For example
+  sequence, you can use the combinator @{ML_ind  EVERY'}. For example
   the function @{ML foo_tac'} from page~\pageref{tac:footacprime} can also 
   be written as:
 *}
@@ -802,11 +802,11 @@
 text {*
   and call @{ML foo_tac1}.  
 
-  With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML_ind [index] EVERY1} it must be
+  With the combinators @{ML THEN'}, @{ML EVERY'} and @{ML_ind  EVERY1} it must be
   guaranteed that all component tactics successfully apply; otherwise the
   whole tactic will fail. If you rather want to try out a number of tactics,
-  then you can use the combinator @{ML_ind [index] ORELSE'} for two tactics, and @{ML_ind
-  [index] FIRST'} (or @{ML_ind [index] FIRST1}) for a list of tactics. For example, the tactic
+  then you can use the combinator @{ML_ind  ORELSE'} for two tactics, and @{ML_ind
+   FIRST'} (or @{ML_ind  FIRST1}) for a list of tactics. For example, the tactic
 
 *}
 
@@ -858,7 +858,7 @@
 text {* 
   Since such repeated applications of a tactic to the reverse order of 
   \emph{all} subgoals is quite common, there is the tactic combinator 
-  @{ML_ind [index] ALLGOALS} that simplifies this. Using this combinator you can simply 
+  @{ML_ind  ALLGOALS} that simplifies this. Using this combinator you can simply 
   write: *}
 
 lemma shows "A \<and> B" and "A \<longrightarrow> B \<longrightarrow>C" and "\<forall>x. D x" and "E \<Longrightarrow> F"
@@ -871,7 +871,7 @@
 text {*
   Remember that we chose to implement @{ML select_tac'} so that it 
   always  succeeds by adding @{ML all_tac} at the end of the tactic
-  list. The same can be achieved with the tactic combinator @{ML_ind [index] TRY}.
+  list. The same can be achieved with the tactic combinator @{ML_ind  TRY}.
   For example:
 *}
 
@@ -904,7 +904,7 @@
   from the end of the theorem list. As a result @{ML select_tac'} would only
   succeed on goals where it can make progress. But for the sake of argument,
   let us suppose that this deletion is \emph{not} an option. In such cases, you can
-  use the combinator @{ML_ind [index] CHANGED} to make sure the subgoal has been changed
+  use the combinator @{ML_ind  CHANGED} to make sure the subgoal has been changed
   by the tactic. Because now
 
 *}
@@ -922,7 +922,7 @@
 text {*
   We can further extend @{ML select_tac'} so that it not just applies to the topmost
   connective, but also to the ones immediately ``underneath'', i.e.~analyse the goal 
-  completely. For this you can use the tactic combinator @{ML_ind [index] REPEAT}. As an example 
+  completely. For this you can use the tactic combinator @{ML_ind  REPEAT}. As an example 
   suppose the following tactic
 *}
 
@@ -943,7 +943,7 @@
   Here it is crucial that @{ML select_tac'} is prefixed with @{ML CHANGED}, 
   because otherwise @{ML REPEAT} runs into an infinite loop (it applies the
   tactic as long as it succeeds). The function
-  @{ML_ind [index] REPEAT1} is similar, but runs the tactic at least once (failing if 
+  @{ML_ind  REPEAT1} is similar, but runs the tactic at least once (failing if 
   this is not possible).
 
   If you are after the ``primed'' version of @{ML repeat_xmp_tac}, then you 
@@ -959,7 +959,7 @@
   and @{ML repeat_xmp_tac'} are not yet quite what we are after: the problem is
   that goals 2 and 3 are not analysed. This is because the tactic
   is applied repeatedly only to the first subgoal. To analyse also all
-  resulting subgoals, you can use the tactic combinator @{ML_ind [index] REPEAT_ALL_NEW}. 
+  resulting subgoals, you can use the tactic combinator @{ML_ind  REPEAT_ALL_NEW}. 
   Suppose the tactic
 *}
 
@@ -1012,7 +1012,7 @@
   Sometimes this leads to confusing behaviour of tactics and also has
   the potential to explode the search space for tactics.
   These problems can be avoided by prefixing the tactic with the tactic 
-  combinator @{ML_ind [index] DETERM}.
+  combinator @{ML_ind  DETERM}.
 *}
 
 lemma "\<lbrakk>P1 \<or> Q1; P2 \<or> Q2\<rbrakk> \<Longrightarrow> R"
@@ -1049,7 +1049,7 @@
 text {*
   then the tactic @{ML select_tac''} will be tried out and any failure is harnessed. 
   We again have to use the construction with \mbox{@{text "TRY o ..."}} since there is 
-  no primed version of @{ML_ind [index] TRY}. The tactic combinator @{ML_ind [index] TRYALL} will try out
+  no primed version of @{ML_ind  TRY}. The tactic combinator @{ML_ind  TRYALL} will try out
   a tactic on all subgoals. For example the tactic 
 *}
 
@@ -1058,7 +1058,7 @@
 text {*
   will solve all trivial subgoals involving @{term True} or @{term "False"}.
 
-  (FIXME: say something about @{ML_ind [index] COND} and COND')
+  (FIXME: say something about @{ML_ind  COND} and COND')
 
   (FIXME: PARALLEL-CHOICE PARALLEL-GOALS)
   
@@ -1118,7 +1118,7 @@
   are discharged.  Note that in Isabelle the left-rules need to be implemented
   as elimination rules. You need to prove separate lemmas corresponding to
   $\longrightarrow_{L_{1..4}}$.  In order to explore all possibilities of applying 
-  the rules, use the tactic combinator @{ML_ind [index] DEPTH_SOLVE}, which searches 
+  the rules, use the tactic combinator @{ML_ind  DEPTH_SOLVE}, which searches 
   for a state in which all subgoals are solved. Add also rules for equality and
   run your tactic on the de Bruijn formulae discussed in Exercise~\ref{ex:debruijn}. 
   \end{exercise}
@@ -1142,11 +1142,11 @@
   \begin{isabelle}
   \begin{center}
   \begin{tabular}{l@ {\hspace{2cm}}l}
-   @{ML_ind [index] simp_tac}            & @{text "(simp (no_asm))"} \\
-   @{ML_ind [index] asm_simp_tac}        & @{text "(simp (no_asm_simp))"} \\
-   @{ML_ind [index] full_simp_tac}       & @{text "(simp (no_asm_use))"} \\
-   @{ML_ind [index] asm_lr_simp_tac}     & @{text "(simp (asm_lr))"} \\
-   @{ML_ind [index] asm_full_simp_tac}   & @{text "(simp)"}
+   @{ML_ind  simp_tac}            & @{text "(simp (no_asm))"} \\
+   @{ML_ind  asm_simp_tac}        & @{text "(simp (no_asm_simp))"} \\
+   @{ML_ind  full_simp_tac}       & @{text "(simp (no_asm_use))"} \\
+   @{ML_ind  asm_lr_simp_tac}     & @{text "(simp (asm_lr))"} \\
+   @{ML_ind  asm_full_simp_tac}   & @{text "(simp)"}
   \end{tabular}
   \end{center}
   \end{isabelle}
@@ -1230,9 +1230,9 @@
 
   \begin{isabelle}
   \begin{tabular}{ll}
-  @{ML_ind [index] addsimps}    & @{ML_ind [index] delsimps}\\
-  @{ML_ind [index] addcongs}    & @{ML_ind [index] delcongs}\\
-  @{ML_ind [index] addsimprocs} & @{ML_ind [index] delsimprocs}\\
+  @{ML_ind  addsimps}    & @{ML_ind  delsimps}\\
+  @{ML_ind  addcongs}    & @{ML_ind  delcongs}\\
+  @{ML_ind  addsimprocs} & @{ML_ind  delsimprocs}\\
   \end{tabular}
   \end{isabelle}
 
@@ -1262,7 +1262,7 @@
 text_raw {* 
 \end{isabelle}
 \end{minipage}
-\caption{The function @{ML_ind [index] dest_ss in Simplifier} returns a record containing
+\caption{The function @{ML_ind  dest_ss in Simplifier} returns a record containing
   all printable information stored in a simpset. We are here only interested in the 
   simplification rules, congruence rules and simprocs.\label{fig:printss}}
 \end{figure} *}
@@ -1270,7 +1270,7 @@
 text {* 
   To see how they work, consider the function in Figure~\ref{fig:printss}, which
   prints out some parts of a simpset. If you use it to print out the components of the
-  empty simpset, i.e., @{ML_ind [index] empty_ss}
+  empty simpset, i.e., @{ML_ind  empty_ss}
   
   @{ML_response_fake [display,gray]
   "print_ss @{context} empty_ss"
@@ -1317,7 +1317,7 @@
   expects this form of the simplification and congruence rules. However, even 
   when adding these lemmas to @{ML empty_ss} we do not end up with anything useful yet.
 
-  In the context of HOL, the first really useful simpset is @{ML_ind [index] HOL_basic_ss}. While
+  In the context of HOL, the first really useful simpset is @{ML_ind  HOL_basic_ss}. While
   printing out the components of this simpset
 
   @{ML_response_fake [display,gray]
@@ -1344,9 +1344,9 @@
 
 text {*
   This behaviour is not because of simplification rules, but how the subgoaler, solver 
-  and looper are set up in @{ML_ind [index] HOL_basic_ss}.
+  and looper are set up in @{ML_ind  HOL_basic_ss}.
 
-  The simpset @{ML_ind [index] HOL_ss} is an extension of @{ML HOL_basic_ss} containing 
+  The simpset @{ML_ind  HOL_ss} is an extension of @{ML HOL_basic_ss} containing 
   already many useful simplification and congruence rules for the logical 
   connectives in HOL. 
 
@@ -1366,7 +1366,7 @@
 
   
   The simplifier is often used to unfold definitions in a proof. For this the
-  simplifier implements the tactic @{ML_ind [index] rewrite_goals_tac}.\footnote{FIXME: 
+  simplifier implements the tactic @{ML_ind  rewrite_goals_tac}.\footnote{FIXME: 
   see LocalDefs infrastructure.} Suppose for example the
   definition
 *}
@@ -1680,7 +1680,7 @@
   Here the pattern is given as @{ML_type term} (instead of @{ML_type cterm}).
   The function also takes a list of patterns that can trigger the simproc.
   Now the simproc is set up and can be explicitly added using
-  @{ML_ind [index] addsimprocs} to a simpset whenever
+  @{ML_ind  addsimprocs} to a simpset whenever
   needed. 
 
   Simprocs are applied from inside to outside and from left to right. You can
@@ -1766,7 +1766,7 @@
   | dest_suc_trm t = snd (HOLogic.dest_number t)*}
 
 text {* 
-  It uses the library function @{ML_ind [index] dest_number in HOLogic} that transforms
+  It uses the library function @{ML_ind  dest_number in HOLogic} that transforms
   (Isabelle) terms, like @{term "0::nat"}, @{term "1::nat"}, @{term "2::nat"} and so
   on, into integer values. This function raises the exception @{ML TERM}, if
   the term is not a number. The next function expects a pair consisting of a term
@@ -1886,21 +1886,21 @@
 
 text {*
   whereby the produced theorem is always a meta-equality. A simple conversion
-  is the function @{ML_ind [index] all_conv in Conv}, which maps a @{ML_type cterm} to an
+  is the function @{ML_ind  all_conv in Conv}, which maps a @{ML_type cterm} to an
   instance of the (meta)reflexivity theorem. For example:
 
   @{ML_response_fake [display,gray]
   "Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
   "Foo \<or> Bar \<equiv> Foo \<or> Bar"}
 
-  Another simple conversion is @{ML_ind [index] no_conv in Conv} which always raises the 
+  Another simple conversion is @{ML_ind  no_conv in Conv} which always raises the 
   exception @{ML CTERM}.
 
   @{ML_response_fake [display,gray]
   "Conv.no_conv @{cterm True}" 
   "*** Exception- CTERM (\"no conversion\", []) raised"}
 
-  A more interesting conversion is the function @{ML_ind [index] beta_conversion in Thm}: it 
+  A more interesting conversion is the function @{ML_ind  beta_conversion in Thm}: it 
   produces a meta-equation between a term and its beta-normal form. For example
 
   @{ML_response_fake [display,gray]
@@ -1942,7 +1942,7 @@
 
   The main point of conversions is that they can be used for rewriting
   @{ML_type cterm}s. One example is the function 
-  @{ML_ind [index] rewr_conv in Conv}, which expects a meta-equation as an 
+  @{ML_ind  rewr_conv in Conv}, which expects a meta-equation as an 
   argument. Suppose the following meta-equation.
   
 *}
@@ -1961,15 +1961,15 @@
 end"
   "True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
 
-  Note, however, that the function @{ML_ind [index] rewr_conv in Conv} only rewrites the 
+  Note, however, that the function @{ML_ind  rewr_conv in Conv} only rewrites the 
   outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match 
   exactly the 
-  left-hand side of the theorem, then  @{ML_ind [index] rewr_conv in Conv} fails, raising 
+  left-hand side of the theorem, then  @{ML_ind  rewr_conv in Conv} fails, raising 
   the exception @{ML CTERM}.
 
   This very primitive way of rewriting can be made more powerful by
   combining several conversions into one. For this you can use conversion
-  combinators. The simplest conversion combinator is @{ML_ind [index] then_conv}, 
+  combinators. The simplest conversion combinator is @{ML_ind  then_conv}, 
   which applies one conversion after another. For example
 
   @{ML_response_fake [display,gray]
@@ -1986,7 +1986,7 @@
   @{thm [source] true_conj1}. (When running this example recall the 
   problem with the pretty-printer normalising all terms.)
 
-  The conversion combinator @{ML_ind [index] else_conv} tries out the 
+  The conversion combinator @{ML_ind  else_conv} tries out the 
   first one, and if it does not apply, tries the second. For example 
 
   @{ML_response_fake [display,gray]
@@ -2004,7 +2004,7 @@
   does not fail, however, because the combinator @{ML else_conv in Conv} will then 
   try out @{ML all_conv in Conv}, which always succeeds.
 
-  The conversion combinator @{ML_ind [index] try_conv in Conv} constructs a conversion 
+  The conversion combinator @{ML_ind  try_conv in Conv} constructs a conversion 
   which is tried out on a term, but in case of failure just does nothing.
   For example
   
@@ -2020,8 +2020,8 @@
   Apart from the function @{ML beta_conversion in Thm}, which is able to fully
   beta-normalise a term, the conversions so far are restricted in that they
   only apply to the outer-most level of a @{ML_type cterm}. In what follows we
-  will lift this restriction. The combinators @{ML_ind [index] fun_conv in Conv} 
-  and @{ML_ind [index] arg_conv in Conv} will apply
+  will lift this restriction. The combinators @{ML_ind  fun_conv in Conv} 
+  and @{ML_ind  arg_conv in Conv} will apply
   a conversion to the first, respectively second, argument of an application.  
   For example
 
@@ -2040,7 +2040,7 @@
   stands for @{term "True \<and> Q"}. The function @{ML fun_conv in Conv} would apply
   the conversion to the term @{text "(Const \<dots> $ t1)"}.
 
-  The function @{ML_ind [index] abs_conv in Conv} applies a conversion under an 
+  The function @{ML_ind  abs_conv in Conv} applies a conversion under an 
   abstraction. For example:
 
   @{ML_response_fake [display,gray]
@@ -2056,10 +2056,10 @@
   conversion as @{text "(K conv)"}, which is a function that ignores its
   argument (the argument being a sufficiently freshened version of the
   variable that is abstracted and a context). The conversion that goes under
-  an application is @{ML_ind [index] combination_conv in Conv}. It expects two
+  an application is @{ML_ind  combination_conv in Conv}. It expects two
   conversions as arguments, each of which is applied to the corresponding
   ``branch'' of the application. An abbreviation for this conversion is the
-  function @{ML_ind [index] comb_conv in Conv}, which applies the same conversion
+  function @{ML_ind  comb_conv in Conv}, which applies the same conversion
   to both branches.
 
   We can now apply all these functions in a conversion that recursively
@@ -2124,7 +2124,7 @@
 
 text {*
   So far we only applied conversions to @{ML_type cterm}s. Conversions can, however, 
-  also work on theorems using the function @{ML_ind [index] fconv_rule in Conv}. As an example, 
+  also work on theorems using the function @{ML_ind  fconv_rule in Conv}. As an example, 
   consider the conversion @{ML all_true1_conv} and the lemma:
 *}
 
@@ -2144,18 +2144,18 @@
   "?P \<or> \<not> ?P"}
 
   Finally, conversions can also be turned into tactics and then applied to
-  goal states. This can be done with the help of the function @{ML_ind [index] CONVERSION},
+  goal states. This can be done with the help of the function @{ML_ind  CONVERSION},
   and also some predefined conversion combinators that traverse a goal
   state. The combinators for the goal state are: 
 
   \begin{itemize}
-  \item @{ML_ind [index] params_conv in Conv} for converting under parameters
+  \item @{ML_ind  params_conv in Conv} for converting under parameters
   (i.e.~where goals are of the form @{text "\<And>x. P x \<Longrightarrow> Q x"})
 
-  \item @{ML_ind [index] prems_conv in Conv} for applying a conversion to all
+  \item @{ML_ind  prems_conv in Conv} for applying a conversion to all
   premises of a goal, and
 
-  \item @{ML_ind [index] concl_conv in Conv} for applying a conversion to the
+  \item @{ML_ind  concl_conv in Conv} for applying a conversion to the
   conclusion of a goal.
   \end{itemize}
 




