--- a/ProgTutorial/Package/Ind_Code.thy	Sat Oct 31 11:37:41 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Sun Nov 01 10:49:25 2009 +0100
@@ -453,7 +453,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_ind  subst_free}. Line 14 and 15 just iterate 
+  (Line 11) using the function @{ML_ind subst_free in Term}. 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"} 
@@ -599,7 +599,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_ind  SUBPROOF}, since this tactic provides us with the parameters (as
+  tactic @{ML_ind SUBPROOF in Subgoal}, 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 with @{ML SUBPROOF}, however, is that it always expects us to 
   completely discharge the goal (see Section~\ref{sec:simpletacs}). This is 
@@ -638,7 +638,7 @@
   going in our example, we will print out these values using the printing
   function in Figure~\ref{fig:chopprint}. Since @{ML FOCUS in Subgoal} will
   supply us the @{text "params"} and @{text "prems"} as lists, we can 
-  separate them using the function @{ML_ind  chop}. 
+  separate them using the function @{ML_ind chop in Library}. 
 *}
 
 ML %linenosgray{*fun chop_test_tac preds rules =
@@ -869,7 +869,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_ind  MRS} does nothing. Similarly, in the 
+  just the empty list and the function @{ML_ind MRS in Drule} 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
@@ -948,7 +948,7 @@
 end*}
 
 text {*
-  The iteration is done with the function @{ML_ind  map_index} since we
+  The iteration is done with the function @{ML_ind map_index in Library} 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