--- 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], [])]))