--- a/CookBook/Package/simple_inductive_package.ML	Fri Mar 06 21:52:17 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML	Sun Mar 08 20:53:00 2009 +0000
@@ -21,10 +21,10 @@
 fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P 
 
 (* @chunk definitions_aux *) 
-fun definitions_aux s ((binding, syn), (attr, trm)) lthy =
+fun definitions_aux ((binding, syn), trm) lthy =
 let 
   val ((_, (_, thm)), lthy) = 
-                LocalTheory.define s ((binding, syn), (attr, trm)) lthy
+    LocalTheory.define Thm.internalK ((binding, syn), (Attrib.empty_binding, trm)) lthy
 in 
   (thm, lthy) 
 end
@@ -45,7 +45,7 @@
       val t2 = fold_rev mk_all preds' t1;      
       val t3 = fold_rev lambda (params @ zs) t2;
     in
-      definitions_aux Thm.internalK ((R, syn), (Attrib.empty_binding, t3))
+      definitions_aux ((R, syn), t3)
     end) (preds ~~ preds' ~~ Tss) lthy
 end
 (* @end *)