
diff -r ef1da1abee46 -r 1fb8d62c88a0 ProgTutorial/Package/Ind_Code.thy
--- a/ProgTutorial/Package/Ind_Code.thy	Sat May 30 11:12:46 2009 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Sat May 30 17:40:20 2009 +0200
@@ -21,7 +21,7 @@
 
   and then ``register'' the definition inside a local theory. 
   To do the latter, we use the following wrapper for the function
-  @{ML LocalTheory.define}. The wrapper takes a predicate name, a syntax
+  @{ML [index] define in LocalTheory}. The wrapper takes a predicate name, a syntax
   annotation and a term representing the right-hand side of the definition.
 *}
 
@@ -35,12 +35,12 @@
 
 text {*
   It returns the definition (as a theorem) and the local theory in which the
-  definition has been made. In Line 4, @{ML internalK in Thm} is a flag
-  attached to the theorem (others possibile flags are @{ML definitionK in Thm}
-  and @{ML axiomK in Thm}). These flags just classify theorems and have no
+  definition has been made. In Line 4, @{ML [index] internalK in Thm} is a flag
+  attached to the theorem (others possibile flags are @{ML [index] definitionK in Thm}
+  and @{ML [index] axiomK in Thm}). These flags just classify theorems and have no
   significant meaning, except for tools that, for example, find theorems in
   the theorem database.\footnote{FIXME: put in the section about theorems.} We
-  also use @{ML empty_binding in Attrib} in Line 3, since the definitions for
+  also use @{ML [index] empty_binding in Attrib} in Line 3, since the definitions for
   our inductive predicates are not meant to be seen by the user and therefore
   do not need to have any theorem attributes. A testcase for this function is
 *}
@@ -170,7 +170,7 @@
   into the object logic (since definitions cannot be stated with
   meta-connectives). To do this transformation we have to obtain the theory
   behind the local theory (Line 3); with this theory we can use the function
-  @{ML ObjectLogic.atomize_term} to make the transformation (Line 4). The call
+  @{ML [index] atomize_term in ObjectLogic} to make the transformation (Line 4). The call
   to @{ML defn_aux} in Line 5 produces all right-hand sides of the
   definitions. The actual definitions are then made in Line 7.  The result of
   the function is a list of theorems and a local theory (the theorems are
@@ -437,7 +437,7 @@
   the new predicates. In Line 8, we construct the types of these new predicates
   using the given argument types. Next we turn them into terms and subsequently
   certify them (Line 9 and 10). We can now produce the substituted introduction rules 
-  (Line 11) using the function @{ML subst_free}. Line 14 and 15 just iterate 
+  (Line 11) using the function @{ML [index] subst_free}. Line 14 and 15 just iterate 
   the proofs for all predicates.
   From this we obtain a list of theorems. Finally we need to export the 
   fixed variables @{text "Ps"} to obtain the schematic variables @{text "?Ps"} 
@@ -579,7 +579,7 @@
   differently. In the code below we will therefore separate them into @{text
   "params1"} and @{text params2}, respectively @{text "prems1"} and @{text
   "prems2"}. To do this separation, it is best to open a subproof with the
-  tactic @{ML SUBPROOF}, since this tactic provides us with the parameters (as
+  tactic @{ML [index] SUBPROOF}, since this tactic provides us with the parameters (as
   list of @{ML_type cterm}s) and the assumptions (as list of @{ML_type thm}s). 
   The problem we have to overcome with @{ML SUBPROOF}
   is, however, that this tactic always expects us to completely discharge the
@@ -627,7 +627,7 @@
   going in our example, we will print out these values using the printing
   function in Figure~\ref{fig:chopprint}. Since the tactic @{ML SUBPROOF} will
   supply us the @{text "params"} and @{text "prems"} as lists, we can 
-  separate them using the function @{ML chop}. 
+  separate them using the function @{ML [index] chop}. 
 *}
 
 ML{*fun chop_test_tac preds rules =
@@ -691,7 +691,7 @@
 
   To use this premise with @{ML rtac}, we need to instantiate its 
   quantifiers (with @{text params1}) and transform it into rule 
-  format (using @{ML "ObjectLogic.rulify"}. So we can modify the 
+  format (using @{ML [index] rulify in ObjectLogic}. So we can modify the 
   subproof as follows:
 *}
 
@@ -854,7 +854,7 @@
   In Line 4 we use the @{text prems} from the @{ML SUBPROOF} and resolve 
   them with @{text prem}. In the simple cases, that is where the @{text prem} 
   comes from a non-recursive premise of the rule, @{text prems} will be 
-  just the empty list and the function @{ML MRS} does nothing. Similarly, in the 
+  just the empty list and the function @{ML [index] MRS} does nothing. Similarly, in the 
   cases where the recursive premises of the rule do not have preconditions. 
   In case there are preconditions, then Line 4 discharges them. After
   that we can proceed as before, i.e., check whether the outermost
@@ -932,7 +932,7 @@
 end*}
 
 text {*
-  The iteration is done with the function @{ML map_index} since we
+  The iteration is done with the function @{ML [index] map_index} since we
   need the introduction rule together with its number (counted from
   @{text 0}). This completes the code for the functions deriving the
   reasoning infrastructure. It remains to implement some administrative
@@ -945,7 +945,7 @@
   We have produced various theorems (definitions, induction principles and
   introduction rules), but apart from the definitions, we have not yet 
   registered them with the theorem database. This is what the functions 
-  @{ML LocalTheory.note} does. 
+  @{ML [index] note in LocalTheory} does. 
 
 
   For convenience, we use the following 
@@ -1027,7 +1027,7 @@
   Line 20 add further every introduction rule under its own name
   (given by the user).\footnote{FIXME: what happens if the user did not give
   any name.} Line 21 registers the induction principles. For this we have
-  to use some specific attributes. The first @{ML "case_names" in RuleCases} 
+  to use some specific attributes. The first @{ML [index] case_names in RuleCases} 
   corresponds to the case names that are used by Isar to reference the proof
   obligations in the induction. The second @{ML "consumes 1" in RuleCases}
   indicates that the first premise of the induction principle (namely




