--- a/CookBook/Package/Ind_Interface.thy	Sat Dec 13 01:33:22 2008 +0000
+++ b/CookBook/Package/Ind_Interface.thy	Mon Dec 15 10:48:27 2008 +0100
@@ -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 Name.binding}. Strings can be turned into elements of the type
-@{ML_type Name.binding} using the function
-@{ML [display] "Name.binding : string -> Name.binding"}
+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"}
 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 "Name.binding * Attrib.src list"}.
+introduction rules is just a shorthand for the type @{ML_type "Binding.T * 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:
-  (Name.binding * string option * mixfix) list ->  (*{variables}*)
+  (Binding.T * string option * mixfix) list ->  (*{variables}*)
   (Attrib.binding * string list) list list ->  (*{rules}*)
   local_theory ->
-  (((Name.binding * typ) * mixfix) list *
+  (((Binding.T * typ) * mixfix) list *
    (Attrib.binding * term list) list) *
   local_theory"}
 *}
@@ -108,10 +108,10 @@
 function to parse the introduction rules of the @{text trcl} predicate:
 @{ML_response [display]
 "Specification.read_specification
-  [(Name.binding \"trcl\", NONE, NoSyn),
-   (Name.binding \"r\", SOME \"'a \<Rightarrow> 'a \<Rightarrow> bool\", NoSyn)]
-  [[((Name.binding \"base\", []), [\"trcl r x x\"])],
-   [((Name.binding \"step\", []), [\"trcl r x y \<Longrightarrow> r y z \<Longrightarrow> trcl r x z\"])]]
+  [(Binding.name \"trcl\", NONE, NoSyn),
+   (Binding.name \"r\", SOME \"'a \<Rightarrow> 'a \<Rightarrow> bool\", NoSyn)]
+  [[((Binding.name \"base\", []), [\"trcl r x x\"])],
+   [((Binding.name \"step\", []), [\"trcl r x y \<Longrightarrow> r y z \<Longrightarrow> trcl r x z\"])]]
   @{context}"
 "((\<dots>,
   [(\<dots>,
@@ -127,7 +127,7 @@
                (Free (\"trcl\", \<dots>) $ Free (\"r\", \<dots>) $ Bound 2 $ Bound 1)) $
              (Const (\"==>\", \<dots>) $ \<dots> $ \<dots>))))])]),
  \<dots>)
-: (((Name.binding * typ) * mixfix) list *
+: (((Binding.T * 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
@@ -249,8 +249,8 @@
 
 ML {*
 val (result, lthy) = SimpleInductivePackage.add_inductive
-  [(Name.binding "trcl'", NONE, NoSyn)] [(Name.binding "r", SOME "'a \<Rightarrow> 'a \<Rightarrow> bool", NoSyn)]
-  [((Name.binding "base", []), "\<And>x. trcl' r x x"), ((Name.binding "step", []), "\<And>x y z. trcl' r x y \<Longrightarrow> r y z \<Longrightarrow> trcl' r x z")]
+  [(Binding.name "trcl'", NONE, NoSyn)] [(Binding.name "r", SOME "'a \<Rightarrow> 'a \<Rightarrow> bool", NoSyn)]
+  [((Binding.name "base", []), "\<And>x. trcl' r x x"), ((Binding.name "step", []), "\<And>x y z. trcl' r x y \<Longrightarrow> r y z \<Longrightarrow> trcl' r x z")]
   (TheoryTarget.init NONE @{theory})
 *}
 (*>*)
@@ -378,9 +378,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 ->
-  (Name.binding * string option * mixfix) list * token list" in OuterParse} \\
+  (Binding.T * string option * mixfix) list * token list" in OuterParse} \\
 @{ML "for_fixes: token list ->
-  (Name.binding * string option * mixfix) list * token list" in OuterParse} \\
+  (Binding.T * string option * mixfix) list * token list" in OuterParse} \\
 @{ML "!!! : (token list -> 'a) -> token list -> 'a" in OuterParse}
 \end{mytable}
 The parsers @{ML "$$$" in OuterParse} and @{ML "!!!" in OuterParse} are