--- a/CookBook/Package/simple_inductive_package.ML	Sat Feb 14 00:24:05 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML	Sat Feb 14 13:20:21 2009 +0000
@@ -20,17 +20,21 @@
 
 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P 
 
-(* @chunk definitions *) 
-fun define_aux s ((binding, syn), (attr, trm)) lthy =
+(* @chunk definitions_aux *) 
+fun definitions_aux s ((binding, syn), (attr, trm)) lthy =
 let 
-  val ((_, (_ , thm)), lthy) = LocalTheory.define s ((binding, syn), (attr, trm)) lthy
+  val ((_, (_, thm)), lthy) = 
+                LocalTheory.define s ((binding, syn), (attr, trm)) lthy
 in 
   (thm, lthy) 
 end
+(* @end *)
 
-fun DEFINITION params' rules preds preds' Tss lthy =
+(* @chunk definitions *) 
+fun definitions params rules preds preds' Tss lthy =
 let
-  val rules' = map (ObjectLogic.atomize_term (ProofContext.theory_of lthy)) rules
+  val thy = ProofContext.theory_of lthy
+  val rules' = map (ObjectLogic.atomize_term thy) rules
 in
   fold_map (fn ((((R, _), syn), pred), Ts) =>
     let 
@@ -39,9 +43,9 @@
       val t0 = list_comb (pred, zs);
       val t1 = fold_rev (curry HOLogic.mk_imp) rules' t0;
       val t2 = fold_rev mk_all preds' t1;      
-      val t3 = fold_rev lambda (params' @ zs) t2;
+      val t3 = fold_rev lambda (params @ zs) t2;
     in
-      define_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3))
+      definitions_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3))
     end) (preds ~~ preds' ~~ Tss) lthy
 end
 (* @end *)
@@ -125,7 +129,7 @@
     val Tss = map (binder_types o fastype_of) preds';   
     val (ass,rules) = split_list specs;    
 
-    val (defs, lthy1) = DEFINITION params' rules preds preds' Tss lthy
+    val (defs, lthy1) = definitions params' rules preds preds' Tss lthy
     val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1;
       
     val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2
@@ -190,7 +194,7 @@
       Toplevel.local_theory loc (add_inductive preds params specs))
 
 val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
-  OuterKeyword.thy_decl ind_decl;
+          OuterKeyword.thy_decl ind_decl
 (* @end *)
 
 end;