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

--- a/CookBook/Package/simple_inductive_package.ML	Sat Dec 13 01:33:22 2008 +0000
+++ b/CookBook/Package/simple_inductive_package.ML	Mon Dec 15 10:48:27 2008 +0100
@@ -2,13 +2,13 @@
 signature SIMPLE_INDUCTIVE_PACKAGE =
 sig
   val add_inductive_i:
-    ((Name.binding * typ) * mixfix) list ->  (*{predicates}*)
-    (Name.binding * typ) list ->  (*{parameters}*)
+    ((Binding.T * typ) * mixfix) list ->  (*{predicates}*)
+    (Binding.T * typ) list ->  (*{parameters}*)
     (Attrib.binding * term) list ->  (*{rules}*)
     local_theory -> (thm list * thm list) * local_theory
   val add_inductive:
-    (Name.binding * string option * mixfix) list ->  (*{predicates}*)
-    (Name.binding * string option * mixfix) list ->  (*{parameters}*)
+    (Binding.T * string option * mixfix) list ->  (*{predicates}*)
+    (Binding.T * string option * mixfix) list ->  (*{parameters}*)
     (Attrib.binding * string) list ->  (*{rules}*)
     local_theory -> (thm list * thm list) * local_theory
 end;
@@ -19,9 +19,9 @@
 
 fun add_inductive_i preds_syn params intrs lthy =
   let
-    val params' = map (fn (p, T) => Free (Name.name_of p, T)) params;
+    val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params;
     val preds = map (fn ((R, T), _) =>
-      list_comb (Free (Name.name_of R, T), params')) preds_syn;
+      list_comb (Free (Binding.base_name R, T), params')) preds_syn;
     val Tss = map (binder_types o fastype_of) preds;
 
     (* making the definition *)
@@ -36,12 +36,12 @@
         (map (pair "z") Ts))
       in
         LocalTheory.define Thm.internalK
-          ((R, syn), (Attrib.no_binding, fold_rev lambda (params' @ zs)
+          ((R, syn), (Attrib.empty_binding, fold_rev lambda (params' @ zs)
             (fold_rev mk_all preds (fold_rev (curry HOLogic.mk_imp)
                intrs' (list_comb (pred, zs)))))) #>> snd #>> snd
        end) (preds_syn ~~ preds ~~ Tss) lthy;
 
-    val (_, lthy2) = Variable.add_fixes (map (Name.name_of o fst) params) lthy1;
+    val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1;
 
 
     (* proving the induction rules *)
@@ -116,18 +116,18 @@
 
     (* storing the theorems *)
 
-    val mut_name = space_implode "_" (map (Name.name_of o fst o fst) preds_syn);
-    val case_names = map (Name.name_of o fst o fst) intrs
+    val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds_syn);
+    val case_names = map (Binding.base_name o fst o fst) intrs
   in
     lthy1 |>
     LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
-      ((Name.qualified mut_name a, atts), [([th], [])]))
+      ((Binding.qualify mut_name a, atts), [([th], [])]))
         (intrs ~~ intr_ths)) |->
     (fn intr_thss => LocalTheory.note Thm.theoremK
-       ((Name.qualified mut_name (Name.binding "intros"), []), maps snd intr_thss)) |>>
+       ((Binding.qualify mut_name (Binding.name "intros"), []), maps snd intr_thss)) |>>
     snd ||>>
     (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
-       ((Name.qualified (Name.name_of R) (Name.binding "induct"),
+       ((Binding.qualify (Binding.base_name R) (Binding.name "induct"),
          [Attrib.internal (K (RuleCases.case_names case_names)),
           Attrib.internal (K (RuleCases.consumes 1)),
           Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))

--- a/CookBook/chunks.ML	Sat Dec 13 01:33:22 2008 +0000
+++ b/CookBook/chunks.ML	Mon Dec 15 10:48:27 2008 +0100
@@ -14,8 +14,9 @@
 );
 
 fun declare_chunk name thy =
-  (Sign.full_name thy name,
-   ChunkData.map (NameSpace.extend_table (Sign.naming_of thy) [(name, ([], stamp ()))]) thy
+  (Sign.full_bname thy name,
+   ChunkData.map (snd o NameSpace.bind (Sign.naming_of thy)
+     (Binding.name name, ([], stamp ()))) thy
    handle Symtab.DUP _ => error ("Duplicate definition of ML chunk " ^ quote name));
 
 fun augment_chunk tok name =

Binary file cookbook.pdf has changed