--- a/CookBook/Package/Ind_Interface.thy	Fri Jan 23 17:50:35 2009 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Sat Jan 24 21:38:52 2009 +0000
@@ -53,12 +53,12 @@
 the predicates and parameters as well. Note that @{ML add_inductive_i in SIP} does not
 allow mixfix syntax to be associated with parameters, since it can only be used
 for parsing. The names of the predicates, parameters and rules are represented by the
-type @{ML_type Binding.T}. Strings can be turned into elements of the type
-@{ML_type Binding.T} using the function
-@{ML [display] "Binding.name : string -> Binding.T"}
+type @{ML_type Binding.binding}. Strings can be turned into elements of the type
+@{ML_type Binding.binding} using the function
+@{ML [display] "Binding.name : string -> Binding.binding"}
 Each introduction rule is given as a tuple containing its name, a list of \emph{attributes}
 and a logical formula. Note that the type @{ML_type Attrib.binding} used in the list of
-introduction rules is just a shorthand for the type @{ML_type "Binding.T * Attrib.src list"}.
+introduction rules is just a shorthand for the type @{ML_type "Binding.binding * Attrib.src list"}.
 The function @{ML add_inductive_i in SIP} expects the formula to be specified using the datatype
 @{ML_type term}, whereas @{ML add_inductive in SIP} expects it to be given as a string.
 An attribute specifies additional actions and transformations that should be applied to
@@ -72,10 +72,10 @@
 @{ML_chunk [display] add_inductive}
 For parsing and type checking the introduction rules, we use the function
 @{ML [display] "Specification.read_specification:
-  (Binding.T * string option * mixfix) list ->  (*{variables}*)
+  (Binding.binding * string option * mixfix) list ->  (*{variables}*)
   (Attrib.binding * string list) list list ->  (*{rules}*)
   local_theory ->
-  (((Binding.T * typ) * mixfix) list *
+  (((Binding.binding * typ) * mixfix) list *
    (Attrib.binding * term list) list) *
   local_theory"}
 *}
@@ -127,7 +127,7 @@
                (Free (\"trcl\", \<dots>) $ Free (\"r\", \<dots>) $ Bound 2 $ Bound 1)) $
              (Const (\"==>\", \<dots>) $ \<dots> $ \<dots>))))])]),
  \<dots>)
-: (((Binding.T * typ) * mixfix) list *
+: (((Binding.binding * typ) * mixfix) list *
    (Attrib.binding * term list) list) * local_theory"}
 In the list of variables passed to @{ML read_specification in Specification}, we have
 used the mixfix annotation @{ML NoSyn} to indicate that we do not want to associate any
@@ -382,9 +382,9 @@
 @{ML "prop: token list -> string * token list" in OuterParse} \\
 @{ML "opt_target: token list -> string option * token list" in OuterParse} \\
 @{ML "fixes: token list ->
-  (Binding.T * string option * mixfix) list * token list" in OuterParse} \\
+  (Binding.binding * string option * mixfix) list * token list" in OuterParse} \\
 @{ML "for_fixes: token list ->
-  (Binding.T * string option * mixfix) list * token list" in OuterParse} \\
+  (Binding.binding * string option * mixfix) list * token list" in OuterParse} \\
 @{ML "!!! : (token list -> 'a) -> token list -> 'a" in OuterParse}
 \end{table}
 

--- 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;