diff -r b071a0b88298 -r 667a0943c40b CookBook/Package/simple_inductive_package.ML
--- a/CookBook/Package/simple_inductive_package.ML	Thu Jan 29 17:08:39 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML	Thu Jan 29 17:09:56 2009 +0000
@@ -42,10 +42,10 @@
        end) (preds_syn ~~ preds ~~ Tss) lthy;
 
     val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1;
-
-
+ 
+     
     (* proving the induction rules *)
-
+    (* @chunk induction_rules *)
     val (Pnames, lthy3) =
       Variable.variant_fixes (replicate (length preds) "P") lthy2;
     val Ps = map (fn (s, Ts) => Free (s, Ts ---> HOLogic.boolT))
@@ -76,10 +76,10 @@
       end;
 
     val indrules = map prove_indrule (preds ~~ Ps ~~ Tss);
-
+    (* @end *)
 
     (* proving the introduction rules *)
-
+    (* @chunk intro_rules *) 
     val all_elims = fold (fn ct => fn th => th RS inst_spec ct);
     val imp_elims = fold (fn th => fn th' => [th', th] MRS mp);
 
@@ -112,12 +112,13 @@
       singleton (ProofContext.export lthy2 lthy1);
 
     val intr_ths = map_index prove_intr intrs;
-
+    (* @end *)
 
     (* storing the theorems *)
-
+    (* @chunk storing *)
     val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds_syn);
     val case_names = map (Binding.base_name o fst o fst) intrs
+    (* @end *)
   in
     lthy1 |>
     LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
@@ -133,7 +134,7 @@
           Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
          (preds_syn ~~ indrules)) #>> maps snd)
   end;
-
+   
 (* @chunk add_inductive *)
 fun add_inductive preds_syn params_syn intro_srcs lthy =
   let