diff -r f2dea0465bb4 -r b99fa5fa63fc CookBook/Package/simple_inductive_package.ML
--- a/CookBook/Package/simple_inductive_package.ML	Fri Jan 23 17:50:35 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML	Sat Jan 24 21:38:52 2009 +0000
@@ -2,13 +2,13 @@
 signature SIMPLE_INDUCTIVE_PACKAGE =
 sig
   val add_inductive_i:
-    ((Binding.T * typ) * mixfix) list ->  (*{predicates}*)
-    (Binding.T * typ) list ->  (*{parameters}*)
+    ((Binding.binding * typ) * mixfix) list ->  (*{predicates}*)
+    (Binding.binding * typ) list ->  (*{parameters}*)
     (Attrib.binding * term) list ->  (*{rules}*)
     local_theory -> (thm list * thm list) * local_theory
   val add_inductive:
-    (Binding.T * string option * mixfix) list ->  (*{predicates}*)
-    (Binding.T * string option * mixfix) list ->  (*{parameters}*)
+    (Binding.binding * string option * mixfix) list ->  (*{predicates}*)
+    (Binding.binding * string option * mixfix) list ->  (*{parameters}*)
     (Attrib.binding * string) list ->  (*{rules}*)
     local_theory -> (thm list * thm list) * local_theory
 end;