--- a/CookBook/Package/Ind_Code.thy	Wed Mar 18 03:27:15 2009 +0100
+++ b/CookBook/Package/Ind_Code.thy	Wed Mar 18 18:27:48 2009 +0100
@@ -65,7 +65,7 @@
 
 local_setup %gray {* fn lthy =>
 let
-  val arg =  ((Binding.name "MyTrue", NoSyn), @{term True})
+  val arg =  ((@{binding "MyTrue"}, NoSyn), @{term True})
   val (def, lthy') = make_defs arg lthy 
 in
   warning (str_of_thm lthy' def); lthy'
@@ -190,7 +190,7 @@
                @{prop "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
                @{prop "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}] 
   val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
-  val prednames = [Binding.name "even", Binding.name "odd"] 
+  val prednames = [@{binding "even"}, @{binding "odd"}] 
   val syns = [NoSyn, NoSyn] 
   val arg_tyss = [[@{typ "nat"}], [@{typ "nat"}]]
   val (defs, lthy') = definitions rules preds prednames syns arg_tyss lthy
@@ -501,7 +501,7 @@
 
 text {* main internal function *}
 
-ML %linenosgray{*fun add_inductive_i pred_specs rule_specs lthy =
+ML %linenosgray{*fun add_inductive pred_specs rule_specs lthy =
 let
   val syns = map snd pred_specs
   val pred_specs' = map fst pred_specs
@@ -522,10 +522,10 @@
     |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
         ((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules)) 
     |-> (fn intross => LocalTheory.note Thm.theoremK
-         ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) 
+         ((Binding.qualify false mut_name (@{binding "intros"}), []), maps snd intross)) 
     |>> snd 
     ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
-         ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"),
+         ((Binding.qualify false (Binding.name_of R) (@{binding "induct"}),
           [Attrib.internal (K (RuleCases.case_names case_names)),
            Attrib.internal (K (RuleCases.consumes 1)),
            Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
@@ -533,12 +533,12 @@
     |> snd
 end*}
 
-ML{*fun add_inductive pred_specs rule_specs lthy =
+ML{*fun add_inductive_cmd pred_specs rule_specs lthy =
 let
   val ((pred_specs', rule_specs'), _) = 
          Specification.read_spec pred_specs rule_specs lthy
 in
-  add_inductive_i pred_specs' rule_specs' lthy
+  add_inductive pred_specs' rule_specs' lthy
 end*} 
 
 ML{*val spec_parser = 
@@ -551,7 +551,7 @@
 
 ML{*val specification =
   spec_parser >>
-    (fn ((pred_specs), rule_specs) => add_inductive pred_specs rule_specs)*}
+    (fn ((pred_specs), rule_specs) => add_inductive_cmd pred_specs rule_specs)*}
 
 ML{*val _ = OuterSyntax.local_theory "simple_inductive" 
               "define inductive predicates"