--- a/CookBook/Package/Ind_Code.thy	Mon Mar 16 03:02:56 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy	Tue Mar 17 01:56:29 2009 +0100
@@ -229,7 +229,7 @@
   For example we can use it to instantiate an assumption:
 *}
 
-lemma "\<forall>x1 x2 x3. P (x1::nat) (x2::nat) (x3::nat) \<Longrightarrow> True"
+lemma "\<forall>(x1::nat) (x2::nat) (x3::nat). P x1 x2 x3 \<Longrightarrow> True"
 apply (tactic {* 
   let 
     val ctrms = [@{cterm "y1::nat"},@{cterm "y2::nat"},@{cterm "y3::nat"}]
@@ -249,7 +249,7 @@
   as follows
 *}
 
-ML{*fun induction_tac defs prems insts =
+ML %linenosgray{*fun induction_tac defs prems insts =
   EVERY1 [ObjectLogic.full_atomize_tac,
           cut_facts_tac prems,
           K (rewrite_goals_tac defs),
@@ -280,17 +280,24 @@
 
   While the generic proof for the induction principle is relatively simple, 
   it is a bit harder to set up the goals just from the given introduction 
-  rules. For this we have to construct
+  rules. For this we have to construct for each predicate @{text "pred"}
 
   @{text [display] 
-  "\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^raw:$P$> \<^raw:$zs$>"}
+  "\<And>\<^raw:$zs$>. pred \<^raw:$zs$> \<Longrightarrow> rules[preds := \<^raw:$Ps$>] \<Longrightarrow> \<^raw:$P$>\<^raw:$zs$>"}
+
+  where the given predicates @{text preds} are replaced by new distinct 
+  ones written as @{text "\<^raw:$Ps$>"}, and also need to be applied to
+  new variables @{text "\<^raw:$zs$>"}. 
 
-  where the given predicates are replaced by new ones written
-  as @{text "\<^raw:$Ps$>"}, and also generate new variables 
-  @{text "\<^raw:$zs$>"}.
+  The function below expects that the rules are already appropriately
+  replaced. The argument @{text "mrules"} stands for these modified
+  introduction rules; @{text cnewpreds} are the certified terms coresponding
+  to the variables @{text "\<^raw:$Ps$>"}; @{text "pred"} is the predicate for
+  which we prove the introduction principle; @{text "newpred"} is its
+  replacement and @{text "tys"} are the types of its argument.
 *}
 
-ML %linenosgray{* fun prove_induction lthy defs rules cnewpreds ((pred, newpred), tys)  =
+ML %linenosgray{* fun prove_induction lthy defs mrules cnewpreds ((pred, newpred), tys)  =
 let
   val zs = replicate (length tys) "z"
   val (newargnames, lthy') = Variable.variant_fixes zs lthy;
@@ -298,14 +305,32 @@
   
   val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))
   val goal = Logic.list_implies 
-         (rules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
+         (mrules, HOLogic.mk_Trueprop (list_comb (newpred, newargs)))
 in
   Goal.prove lthy' [] [prem] goal
   (fn {prems, ...} => induction_tac defs prems cnewpreds)
   |> singleton (ProofContext.export lthy' lthy)
 end *}
 
-text {* *}
+text {* 
+  In Line 3 we produce a list of names @{text "\<^raw:$zs$>"} according to the type 
+  list. Line 4 makes these names unique and declare them as \emph{free} (but fixed)
+  variables. These variables are free in the new theory @{text "lthy'"}. In Line 5
+  we just construct the terms corresponding to the variables. The term variables are
+  applied to the predicate in Line 7 (this is the first premise 
+  @{text "pred \<^raw:$zs$>"} of the induction principle). In Line 8 and 9
+  we first the term  @{text "\<^raw:$P$>\<^raw:$zs$>"} and then add
+  the (modified) introduction rules as premises.
+
+  In Line 11 we set up the goal to be proved; call the induction tactic in
+  Line 13. This returns a theorem. However, it is a theorem proved inside
+  the local theory @{text "lthy'"} where the variables @{text "\<^raw:$zs$>"} are
+  fixed, but free. By exporting this theorem from @{text "lthy'"} (which does contain
+  the  @{text "\<^raw:$zs$>"} as free) to @{text "lthy"} (which does not), we
+  obtain the desired quantifications @{text "\<And>\<^raw:$zs$>"}.
+
+  So it is left to produce the modified rules and 
+*}
 
 ML %linenosgray{*fun inductions rules defs preds tyss lthy1  =
 let