--- a/CookBook/Package/simple_inductive_package.ML	Wed Mar 04 13:50:47 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML	Wed Mar 04 14:26:21 2009 +0000
@@ -124,29 +124,29 @@
 (* @chunk add_inductive_i *)
 fun add_inductive_i preds params specs lthy =
 let
-  val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params;
-  val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.base_name R, T), params')) preds;
+  val params' = map (fn (p, T) => Free (Binding.name_of p, T)) params;
+  val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.name_of R, T), params')) preds;
   val Tss = map (binder_types o fastype_of) preds';   
   val (ass,rules) = split_list specs;    
 
   val (defs, lthy1) = definitions params' rules preds preds' Tss lthy
-  val (_, lthy2) = Variable.add_fixes (map (Binding.base_name o fst) params) lthy1;
+  val (_, lthy2) = Variable.add_fixes (map (Binding.name_of o fst) params) lthy1;
       
   val inducts = INDUCTION rules preds' Tss defs lthy1 lthy2
 
   val intros = INTROS rules preds' defs lthy1 lthy2
 
-  val mut_name = space_implode "_" (map (Binding.base_name o fst o fst) preds);
-  val case_names = map (Binding.base_name o fst o fst) specs
+  val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds);
+  val case_names = map (Binding.name_of o fst o fst) specs
 in
     lthy1 
     |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
-        ((Binding.qualify mut_name a, atts), [([th], [])])) (specs ~~ intros)) 
+        ((Binding.qualify false mut_name a, atts), [([th], [])])) (specs ~~ intros)) 
     |-> (fn intross => LocalTheory.note Thm.theoremK
-         ((Binding.qualify mut_name (Binding.name "intros"), []), maps snd intross)) 
+         ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) 
     |>> snd 
     ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
-         ((Binding.qualify (Binding.base_name R) (Binding.name "induct"),
+         ((Binding.qualify false (Binding.name_of 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], [])]))