--- a/CookBook/Package/simple_inductive_package.ML	Sun Feb 15 18:58:21 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML	Mon Feb 16 17:17:24 2009 +0000
@@ -4,7 +4,7 @@
   val add_inductive_i:
     ((Binding.binding * typ) * mixfix) list ->  (*{predicates}*)
     (Binding.binding * typ) list ->  (*{parameters}*)
-    ((Binding.binding * Attrib.src list) * term) list ->  (*{rules}*)
+    (Attrib.binding * term) list ->  (*{rules}*)
     local_theory -> local_theory
 
   val add_inductive: