# HG changeset patch
# User wenzelm
# Date 1236460645 -3600
# Node ID 76fd85bbf139ae2e437cfdf726ce9e5dde96bd8f
# Parent  10a67c5ddddb8b544c44208c0b6675d92864f8a3
more uniform handling of binding in packages;

diff -r 10a67c5ddddb -r 76fd85bbf139 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -100,7 +100,7 @@
     
     val (_,thy1) = 
     fold_map (fn ak => fn thy => 
-          let val dt = ([],ak,NoSyn,[(ak,[@{typ nat}],NoSyn)]) 
+          let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)])
               val ({inject,case_thms,...},thy1) = DatatypePackage.add_datatype true false [ak] [dt] thy
               val inject_flat = Library.flat inject
               val ak_type = Type (Sign.intern_type thy1 ak,[])
@@ -187,7 +187,7 @@
                     cif $ HOLogic.mk_eq (a,c) $ b $ (cif $ HOLogic.mk_eq (b,c) $ a $ c)))
         val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
       in
-        thy |> Sign.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
+        thy |> Sign.add_consts_i [(Binding.name ("swap_" ^ ak_name), swapT, NoSyn)] 
             |> PureThy.add_defs_unchecked true [((Binding.name name, def2),[])]
             |> snd
             |> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1),[])]
@@ -217,7 +217,7 @@
                    (Const (qu_prm_name, prmT) $ mk_Cons x xs $ a,
                     Const (swap_name, swapT) $ x $ (Const (qu_prm_name, prmT) $ xs $ a)));
       in
-        thy |> Sign.add_consts_i [(prm_name, mk_permT T --> T --> T, NoSyn)] 
+        thy |> Sign.add_consts_i [(Binding.name prm_name, mk_permT T --> T --> T, NoSyn)] 
             |> OldPrimrecPackage.add_primrec_unchecked_i "" [(("", def1), []),(("", def2), [])]
       end) ak_names_types thy3;
     
@@ -300,7 +300,7 @@
                        (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
                         HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
       in
-          AxClass.define_class (cl_name, ["HOL.type"]) []
+          AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
                 [((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
                  ((Binding.name (cl_name ^ "2"), []), [axiom2]),                           
                  ((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
@@ -349,7 +349,8 @@
           val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
 
        in  
-        AxClass.define_class (cl_name, [pt_name]) [] [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy            
+        AxClass.define_class (Binding.name cl_name, [pt_name]) []
+          [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy
        end) ak_names_types thy8; 
          
      (* proves that every fs_<ak>-type together with <ak>-type   *)
@@ -398,7 +399,7 @@
                            (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
                                            cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
                in  
-                 AxClass.define_class (cl_name, ["HOL.type"]) []
+                 AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
                    [((Binding.name (cl_name ^ "1"), []), [ax1])] thy'  
                end) ak_names_types thy) ak_names_types thy12;
 
diff -r 10a67c5ddddb -r 76fd85bbf139 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -197,7 +197,7 @@
     val tmp_thy = thy |>
       Theory.copy |>
       Sign.add_types (map (fn (tvs, tname, mx, _) =>
-        (tname, length tvs, mx)) dts);
+        (Binding.name tname, length tvs, mx)) dts);
 
     val atoms = atoms_of thy;
 
@@ -235,8 +235,8 @@
           Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
       | replace_types T = T;
 
-    val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, tname ^ "_Rep", NoSyn,
-      map (fn (cname, cargs, mx) => (cname ^ "_Rep",
+    val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, Binding.name (tname ^ "_Rep"), NoSyn,
+      map (fn (cname, cargs, mx) => (Binding.name (cname ^ "_Rep"),
         map replace_types cargs, NoSyn)) constrs)) dts';
 
     val new_type_names' = map (fn n => n ^ "_Rep") new_type_names;
@@ -615,7 +615,8 @@
     val (typedefs, thy6) =
       thy4
       |> fold_map (fn ((((name, mx), tvs), (cname, U)), name') => fn thy =>
-          TypedefPackage.add_typedef false (SOME name') (name, map fst tvs, mx)
+          TypedefPackage.add_typedef false (SOME (Binding.name name'))
+            (Binding.name name, map fst tvs, mx)
             (Const ("Collect", (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $
                Const (cname, U --> HOLogic.boolT)) NONE
             (rtac exI 1 THEN rtac CollectI 1 THEN
@@ -800,7 +801,7 @@
           (Const (rep_name, T --> T') $ lhs, rhs));
         val def_name = (NameSpace.base_name cname) ^ "_def";
         val ([def_thm], thy') = thy |>
-          Sign.add_consts_i [(cname', constrT, mx)] |>
+          Sign.add_consts_i [(Binding.name cname', constrT, mx)] |>
           (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
       in (thy', defs @ [def_thm], eqns @ [eqn]) end;
 
@@ -2012,7 +2013,7 @@
     val (reccomb_defs, thy12) =
       thy11
       |> Sign.add_consts_i (map (fn ((name, T), T') =>
-          (NameSpace.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn))
+          (Binding.name (NameSpace.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
           (reccomb_names ~~ recTs ~~ rec_result_Ts))
       |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
           (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
diff -r 10a67c5ddddb -r 76fd85bbf139 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -235,7 +235,7 @@
     val (reccomb_defs, thy2) =
       thy1
       |> Sign.add_consts_i (map (fn ((name, T), T') =>
-          (NameSpace.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
+          (Binding.name (NameSpace.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
           (reccomb_names ~~ recTs ~~ rec_result_Ts))
       |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
           (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
diff -r 10a67c5ddddb -r 76fd85bbf139 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -36,8 +36,8 @@
        simps : thm list} -> Proof.context -> Proof.context) -> string list option -> term list
     -> theory -> Proof.state;
   val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state;
-  val add_datatype : bool -> bool -> string list -> (string list * bstring * mixfix *
-    (bstring * typ list * mixfix) list) list -> theory ->
+  val add_datatype : bool -> bool -> string list -> (string list * binding * mixfix *
+    (binding * typ list * mixfix) list) list -> theory ->
       {distinct : thm list list,
        inject : thm list list,
        exhaustion : thm list,
@@ -46,8 +46,8 @@
        split_thms : (thm * thm) list,
        induction : thm,
        simps : thm list} * theory
-  val add_datatype_cmd : bool -> string list -> (string list * bstring * mixfix *
-    (bstring * string list * mixfix) list) list -> theory ->
+  val add_datatype_cmd : bool -> string list -> (string list * binding * mixfix *
+    (binding * string list * mixfix) list) list -> theory ->
       {distinct : thm list list,
        inject : thm list list,
        exhaustion : thm list,
@@ -566,11 +566,11 @@
 
     val (tyvars, _, _, _)::_ = dts;
     val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
-      let val full_tname = Sign.full_bname tmp_thy (Syntax.type_name tname mx)
+      let val full_tname = Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname)
       in (case duplicates (op =) tvs of
             [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
                   else error ("Mutually recursive datatypes must have same type parameters")
-          | dups => error ("Duplicate parameter(s) for datatype " ^ full_tname ^
+          | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
               " : " ^ commas dups))
       end) dts);
 
@@ -585,13 +585,14 @@
             val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
                 [] => ()
               | vs => error ("Extra type variables on rhs: " ^ commas vs))
-          in (constrs @ [((if flat_names then Sign.full_bname tmp_thy else
-                Sign.full_bname_path tmp_thy tname) (Syntax.const_name cname mx'),
+          in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
+                Sign.full_name_path tmp_thy (Binding.name_of tname))
+                  (Binding.map_name (Syntax.const_name mx') cname),
                    map (dtyp_of_typ new_dts) cargs')],
               constr_syntax' @ [(cname, mx')], sorts'')
-          end handle ERROR msg =>
-            cat_error msg ("The error above occured in constructor " ^ cname ^
-              " of datatype " ^ tname);
+          end handle ERROR msg => cat_error msg
+           ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^
+            " of datatype " ^ quote (Binding.str_of tname));
 
         val (constrs', constr_syntax', sorts') =
           fold prep_constr constrs ([], [], sorts)
@@ -599,11 +600,11 @@
       in
         case duplicates (op =) (map fst constrs') of
            [] =>
-             (dts' @ [(i, (Sign.full_bname tmp_thy (Syntax.type_name tname mx),
+             (dts' @ [(i, (Sign.full_name tmp_thy (Binding.map_name (Syntax.type_name mx) tname),
                 map DtTFree tvs, constrs'))],
               constr_syntax @ [constr_syntax'], sorts', i + 1)
          | dups => error ("Duplicate constructors " ^ commas dups ^
-             " in datatype " ^ tname)
+             " in datatype " ^ quote (Binding.str_of tname))
       end;
 
     val (dts', constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
@@ -676,12 +677,13 @@
 local structure P = OuterParse and K = OuterKeyword in
 
 val datatype_decl =
-  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
-    (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
+  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.binding -- P.opt_infix --
+    (P.$$$ "=" |-- P.enum1 "|" (P.binding -- Scan.repeat P.typ -- P.opt_mixfix));
 
 fun mk_datatype args =
   let
-    val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
+    val names = map
+      (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
     val specs = map (fn ((((_, vs), t), mx), cons) =>
       (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
   in snd o add_datatype_cmd false names specs end;
diff -r 10a67c5ddddb -r 76fd85bbf139 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -15,7 +15,7 @@
   val distinctness_limit_setup : theory -> theory
   val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
     string list -> DatatypeAux.descr list -> (string * sort) list ->
-      (string * mixfix) list -> (string * mixfix) list list -> attribute
+      (binding * mixfix) list -> (binding * mixfix) list list -> attribute
         -> theory -> (thm list list * thm list list * thm list list *
           DatatypeAux.simproc_dist list * thm) * theory
 end;
@@ -192,7 +192,7 @@
     val (typedefs, thy3) = thy2 |>
       parent_path flat_names |>
       fold_map (fn ((((name, mx), tvs), c), name') =>
-          TypedefPackage.add_typedef false (SOME name') (name, tvs, mx)
+          TypedefPackage.add_typedef false (SOME (Binding.name name')) (name, tvs, mx)
             (Collect $ Const (c, UnivT')) NONE
             (rtac exI 1 THEN rtac CollectI 1 THEN
               QUIET_BREADTH_FIRST (has_fewer_prems 1)
@@ -212,7 +212,7 @@
 
     (* isomorphism declarations *)
 
-    val iso_decls = map (fn (T, s) => (s, T --> Univ_elT, NoSyn))
+    val iso_decls = map (fn (T, s) => (Binding.name s, T --> Univ_elT, NoSyn))
       (oldTs ~~ rep_names');
 
     (* constructor definitions *)
diff -r 10a67c5ddddb -r 76fd85bbf139 src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -140,7 +140,7 @@
     val ((size_def_thms, size_def_thms'), thy') =
       thy
       |> Sign.add_consts_i (map (fn (s, T) =>
-           (NameSpace.base_name s, param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
+           (Binding.name (NameSpace.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
            (size_names ~~ recTs1))
       |> PureThy.add_defs false
         (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
diff -r 10a67c5ddddb -r 76fd85bbf139 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -68,8 +68,8 @@
     val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
       (Logic.strip_imp_concl (prop_of (hd intrs))));
     val params = map dest_Var (Library.take (nparms, ts));
-    val tname = space_implode "_" (NameSpace.base_name s ^ "T" :: vs);
-    fun constr_of_intr intr = (NameSpace.base_name (name_of_thm intr),
+    val tname = Binding.name (space_implode "_" (NameSpace.base_name s ^ "T" :: vs));
+    fun constr_of_intr intr = (Binding.name (NameSpace.base_name (name_of_thm intr)),
       map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
         filter_out (equal Extraction.nullT) (map
           (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
@@ -234,7 +234,7 @@
   end;
 
 fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) =
-  if (name: string) = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
+  if Binding.eq_name (name, s) then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
   else x;
 
 fun add_dummies f [] _ thy =
@@ -242,14 +242,14 @@
   | add_dummies f dts used thy =
       thy
       |> f (map snd dts)
-      |-> (fn dtinfo => pair ((map fst dts), SOME dtinfo))
+      |-> (fn dtinfo => pair (map fst dts, SOME dtinfo))
     handle DatatypeAux.Datatype_Empty name' =>
       let
         val name = NameSpace.base_name name';
-        val dname = Name.variant used "Dummy"
+        val dname = Name.variant used "Dummy";
       in
         thy
-        |> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
+        |> add_dummies f (map (add_dummy (Binding.name name) (Binding.name dname)) dts) (dname :: used)
       end;
 
 fun mk_realizer thy vs (name, rule, rrule, rlz, rt) =
@@ -296,7 +296,7 @@
 
     val thy1' = thy1 |>
       Theory.copy |>
-      Sign.add_types (map (fn s => (NameSpace.base_name s, ar, NoSyn)) tnames) |>
+      Sign.add_types (map (fn s => (Binding.name (NameSpace.base_name s), ar, NoSyn)) tnames) |>
       fold (fn s => AxClass.axiomatize_arity
         (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
         Extraction.add_typeof_eqns_i ty_eqs;
@@ -308,7 +308,7 @@
     val ((dummies, dt_info), thy2) =
       thy1
       |> add_dummies
-           (DatatypePackage.add_datatype false false (map #2 dts))
+           (DatatypePackage.add_datatype false false (map (Binding.name_of o #2) dts))
            (map (pair false) dts) []
       ||> Extraction.add_typeof_eqns_i ty_eqs
       ||> Extraction.add_realizes_eqns_i rlz_eqs;
@@ -330,14 +330,17 @@
         (if c = Extraction.nullt then c else list_comb (c, map Var (rev
           (Term.add_vars (prop_of intr) []) \\ params'))) (prop_of intr)))
             (maps snd rss ~~ List.concat constrss);
-    val (rlzpreds, rlzpreds') = split_list
-      (distinct (op = o pairself (#1 o #1)) (map (fn rintr =>
+    val (rlzpreds, rlzpreds') =
+      rintrs |> map (fn rintr =>
         let
-          val Const (s, T) = head_of (HOLogic.dest_Trueprop
-            (Logic.strip_assums_concl rintr));
+          val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr));
           val s' = NameSpace.base_name s;
-          val T' = Logic.unvarifyT T
-        in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
+          val T' = Logic.unvarifyT T;
+        in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end)
+      |> distinct (op = o pairself (#1 o #1))
+      |> map (apfst (apfst (apfst Binding.name)))
+      |> split_list;
+
     val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
       (List.take (snd (strip_comb
         (HOLogic.dest_Trueprop (Logic.strip_assums_concl (hd rintrs)))), nparms));
diff -r 10a67c5ddddb -r 76fd85bbf139 src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -464,7 +464,7 @@
            | NONE => u)) |>
         Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |>
         eta_contract (member op = cs' orf is_pred pred_arities))) intros;
-    val cnames_syn' = map (fn (b, _) => (Binding.map_name (suffix "p") b, NoSyn)) cnames_syn;
+    val cnames_syn' = map (fn (b, _) => (Binding.suffix_name "p" b, NoSyn)) cnames_syn;
     val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
     val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
       InductivePackage.add_ind_def
diff -r 10a67c5ddddb -r 76fd85bbf139 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/record_package.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -1461,9 +1461,10 @@
           Abs_inject=abs_inject, Abs_inverse = abs_inverse, ...} = TypedefPackage.get_info thy name;
         val rewrite_rule = MetaSimplifier.rewrite_rule [rec_UNIV_I, rec_True_simp];
       in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end;
+    val tname = Binding.name (NameSpace.base_name name);
   in
     thy
-    |> TypecopyPackage.add_typecopy (suffix ext_typeN (NameSpace.base_name name), alphas) repT NONE
+    |> TypecopyPackage.add_typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE
     |-> (fn (name, _) => `(fn thy => get_thms thy name))
   end;
 
@@ -1531,9 +1532,9 @@
     (* 1st stage: defs_thy *)
     fun mk_defs () =
       thy
-      |> extension_typedef name repT (alphas@[zeta])
+      |> extension_typedef name repT (alphas @ [zeta])
       ||> Sign.add_consts_i
-            (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
+            (map (Syntax.no_syn o apfst Binding.name) (apfst base ext_decl :: dest_decls @ upd_decls))
       ||>> PureThy.add_defs false
             (map (Thm.no_attributes o apfst Binding.name) (ext_spec :: dest_specs))
       ||>> PureThy.add_defs false
@@ -1895,8 +1896,8 @@
 
     (*record (scheme) type abbreviation*)
     val recordT_specs =
-      [(suffix schemeN bname, alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
-        (bname, alphas, recT0, Syntax.NoSyn)];
+      [(Binding.name (suffix schemeN bname), alphas @ [zeta], rec_schemeT0, Syntax.NoSyn),
+        (Binding.name bname, alphas, recT0, Syntax.NoSyn)];
 
     (*selectors*)
     fun mk_sel_spec (c,T) =
@@ -1937,8 +1938,9 @@
       |> Sign.add_tyabbrs_i recordT_specs
       |> Sign.add_path bname
       |> Sign.add_consts_i
-          (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
-      |> (Sign.add_consts_i o map Syntax.no_syn)
+          (map2 (fn (x, T) => fn mx => (Binding.name x, T, mx))
+            sel_decls (field_syntax @ [Syntax.NoSyn]))
+      |> (Sign.add_consts_i o map (fn (x, T) => (Binding.name x, T, Syntax.NoSyn)))
           (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
       |> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) sel_specs)
       ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs)
diff -r 10a67c5ddddb -r 76fd85bbf139 src/HOL/Tools/typecopy_package.ML
--- a/src/HOL/Tools/typecopy_package.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/typecopy_package.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -14,7 +14,7 @@
     proj: string * typ,
     proj_def: thm
   }
-  val add_typecopy: bstring * string list -> typ -> (bstring * bstring) option
+  val add_typecopy: binding * string list -> typ -> (binding * binding) option
     -> theory -> (string * info) * theory
   val get_typecopies: theory -> string list
   val get_info: theory -> string -> info option
diff -r 10a67c5ddddb -r 76fd85bbf139 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -13,12 +13,12 @@
     Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
     Rep_induct: thm, Abs_induct: thm}
   val get_info: theory -> string -> info option
-  val add_typedef: bool -> string option -> bstring * string list * mixfix ->
-    term -> (bstring * bstring) option -> tactic -> theory -> (string * info) * theory
-  val typedef: (bool * string) * (bstring * string list * mixfix) * term
-    * (string * string) option -> theory -> Proof.state
-  val typedef_cmd: (bool * string) * (bstring * string list * mixfix) * string
-    * (string * string) option -> theory -> Proof.state
+  val add_typedef: bool -> binding option -> binding * string list * mixfix ->
+    term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
+  val typedef: (bool * binding) * (binding * string list * mixfix) * term
+    * (binding * binding) option -> theory -> Proof.state
+  val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string
+    * (binding * binding) option -> theory -> Proof.state
   val interpretation: (string -> theory -> theory) -> theory -> theory
   val setup: theory -> theory
 end;
@@ -51,9 +51,6 @@
 
 (* prepare_typedef *)
 
-fun err_in_typedef msg name =
-  cat_error msg ("The error(s) above occurred in typedef " ^ quote name);
-
 fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
 
 structure TypedefInterpretation = InterpretationFun(type T = string val eq = op =);
@@ -63,10 +60,12 @@
   let
     val _ = Theory.requires thy "Typedef" "typedefs";
     val ctxt = ProofContext.init thy;
-    val full = Sign.full_bname thy;
+
+    val full = Sign.full_name thy;
+    val full_name = full name;
+    val bname = Binding.name_of name;
 
     (*rhs*)
-    val full_name = full name;
     val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
     val setT = Term.fastype_of set;
     val rhs_tfrees = Term.add_tfrees set [];
@@ -81,11 +80,14 @@
       |> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT))
       |> map TFree;
 
-    val tname = Syntax.type_name t mx;
+    val tname = Binding.map_name (Syntax.type_name mx) t;
     val full_tname = full tname;
     val newT = Type (full_tname, map TFree lhs_tfrees);
 
-    val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
+    val (Rep_name, Abs_name) =
+      (case opt_morphs of
+        NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
+      | SOME morphs => morphs);
     val setT' = map Term.itselfT args_setT ---> setT;
     val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
     val RepC = Const (full Rep_name, newT --> oldT);
@@ -97,15 +99,15 @@
     val set' = if def then setC else set;
     val goal' = mk_inhabited set';
     val goal = mk_inhabited set;
-    val goal_pat = mk_inhabited (Var (the_default (name, 0) (Syntax.read_variable name), setT));
+    val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Syntax.read_variable bname), setT));
 
     (*axiomatization*)
-    val typedef_name = "type_definition_" ^ name;
+    val typedef_name = Binding.prefix_name "type_definition_" name;
     val typedefC =
       Const (@{const_name type_definition},
         (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
     val typedef_prop = Logic.mk_implies (goal', HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
-    val typedef_deps = Term.fold_aterms (fn Const c => insert (op =) c | _ => I) set' [];
+    val typedef_deps = Term.add_consts set' [];
 
     (*set definition*)
     fun add_def theory =
@@ -131,7 +133,7 @@
          (Abs_name, oldT --> newT, NoSyn)]
       #> add_def
       #-> (fn set_def =>
-        PureThy.add_axioms [((Binding.name typedef_name, typedef_prop),
+        PureThy.add_axioms [((typedef_name, typedef_prop),
           [Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])]
         ##>> pair set_def)
       ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
@@ -142,21 +144,21 @@
           val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
               Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
             thy1
-            |> Sign.add_path name
+            |> Sign.add_path (Binding.name_of name)
             |> PureThy.add_thms
-              ((map o apfst o apfst) Binding.name [((Rep_name, make @{thm type_definition.Rep}), []),
-                ((Rep_name ^ "_inverse", make @{thm type_definition.Rep_inverse}), []),
-                ((Abs_name ^ "_inverse", make @{thm type_definition.Abs_inverse}), []),
-                ((Rep_name ^ "_inject", make @{thm type_definition.Rep_inject}), []),
-                ((Abs_name ^ "_inject", make @{thm type_definition.Abs_inject}), []),
-                ((Rep_name ^ "_cases", make @{thm type_definition.Rep_cases}),
-                  [RuleCases.case_names [Rep_name], Induct.cases_pred full_name]),
-                ((Abs_name ^ "_cases", make @{thm type_definition.Abs_cases}),
-                  [RuleCases.case_names [Abs_name], Induct.cases_type full_tname]),
-                ((Rep_name ^ "_induct", make @{thm type_definition.Rep_induct}),
-                  [RuleCases.case_names [Rep_name], Induct.induct_pred full_name]),
-                ((Abs_name ^ "_induct", make @{thm type_definition.Abs_induct}),
-                  [RuleCases.case_names [Abs_name], Induct.induct_type full_tname])])
+              [((Rep_name, make @{thm type_definition.Rep}), []),
+                ((Binding.suffix_name "_inverse" Rep_name, make @{thm type_definition.Rep_inverse}), []),
+                ((Binding.suffix_name "_inverse" Abs_name, make @{thm type_definition.Abs_inverse}), []),
+                ((Binding.suffix_name "_inject" Rep_name, make @{thm type_definition.Rep_inject}), []),
+                ((Binding.suffix_name "_inject" Abs_name, make @{thm type_definition.Abs_inject}), []),
+                ((Binding.suffix_name "_cases" Rep_name, make @{thm type_definition.Rep_cases}),
+                  [RuleCases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
+                ((Binding.suffix_name "_cases" Abs_name, make @{thm type_definition.Abs_cases}),
+                  [RuleCases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
+                ((Binding.suffix_name "_induct" Rep_name, make @{thm type_definition.Rep_induct}),
+                  [RuleCases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
+                ((Binding.suffix_name "_induct" Abs_name, make @{thm type_definition.Abs_induct}),
+                  [RuleCases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])]
             ||> Sign.parent_path;
           val info = {rep_type = oldT, abs_type = newT,
             Rep_name = full Rep_name, Abs_name = full Abs_name,
@@ -201,7 +203,8 @@
       |> typedef_result (setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal);
 
   in (set, goal, goal_pat, typedef_result) end
-  handle ERROR msg => err_in_typedef msg name;
+  handle ERROR msg =>
+    cat_error msg ("The error(s) above occurred in typedef " ^ quote (Binding.str_of name));
 
 
 (* add_typedef: tactic interface *)
@@ -245,13 +248,14 @@
 
 val typedef_decl =
   Scan.optional (P.$$$ "(" |--
-      ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
+      ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
         --| P.$$$ ")") (true, NONE) --
-    (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
-    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
+    (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
+    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
 
 fun mk_typedef ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
-  typedef_cmd ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
+  typedef_cmd ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name),
+    (t, vs, mx), A, morphs);
 
 val _ =
   OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)"
diff -r 10a67c5ddddb -r 76fd85bbf139 src/HOLCF/Tools/cont_consts.ML
--- a/src/HOLCF/Tools/cont_consts.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOLCF/Tools/cont_consts.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -52,11 +52,11 @@
    is generated and connected to the other declaration via some translation.
 *)
 fun fix_mixfix (syn                     , T, mx as Infix           p ) =
-               (Syntax.const_name syn mx, T,       InfixName (syn, p))
+               (Syntax.const_name mx syn, T,       InfixName (syn, p))
   | fix_mixfix (syn                     , T, mx as Infixl           p ) =
-               (Syntax.const_name syn mx, T,       InfixlName (syn, p))
+               (Syntax.const_name mx syn, T,       InfixlName (syn, p))
   | fix_mixfix (syn                     , T, mx as Infixr           p ) =
-               (Syntax.const_name syn mx, T,       InfixrName (syn, p))
+               (Syntax.const_name mx syn, T,       InfixrName (syn, p))
   | fix_mixfix decl = decl;
 fun transform decl = let
         val (c, T, mx) = fix_mixfix decl;
@@ -73,7 +73,7 @@
 |   is_contconst (_,_,Binder _) = false
 |   is_contconst (c,T,mx      ) = cfun_arity T >= Syntax.mixfix_args mx
                          handle ERROR msg => cat_error msg ("in mixfix annotation for " ^
-                                               quote (Syntax.const_name c mx));
+                                               quote (Syntax.const_name mx c));
 
 
 (* add_consts(_i) *)
@@ -85,10 +85,9 @@
     val transformed_decls = map transform contconst_decls;
   in
     thy
-    |> Sign.add_consts_i normal_decls
-    |> Sign.add_consts_i (map first transformed_decls)
-    |> Sign.add_syntax_i (map second transformed_decls)
-    |> Sign.add_trrules_i (List.concat (map third transformed_decls))
+    |> (Sign.add_consts_i o map (upd_first Binding.name))
+      (normal_decls @ map first transformed_decls @ map second transformed_decls)
+    |> Sign.add_trrules_i (maps third transformed_decls)
   end;
 
 val add_consts = gen_add_consts Syntax.read_typ_global;
diff -r 10a67c5ddddb -r 76fd85bbf139 src/HOLCF/Tools/domain/domain_extender.ML
--- a/src/HOLCF/Tools/domain/domain_extender.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_extender.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -103,7 +103,7 @@
 			 (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
                    o fst) eqs''';
     val cons''' = map snd eqs''';
-    fun thy_type  (dname,tvars)  = (NameSpace.base_name dname, length tvars, NoSyn);
+    fun thy_type  (dname,tvars)  = (Binding.name (NameSpace.base_name dname), length tvars, NoSyn);
     fun thy_arity (dname,tvars)  = (dname, map (snd o dest_TFree) tvars, pcpoS);
     val thy'' = thy''' |> Sign.add_types     (map thy_type  dtnvs)
 		       |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
@@ -119,7 +119,7 @@
       | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
       | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
     fun one_con (con,mx,args) =
-	((Syntax.const_name con mx),
+	((Syntax.const_name mx con),
 	 ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
 					find_index_eq tp dts,
 					DatatypeAux.dtyp_of_typ new_dts tp),
diff -r 10a67c5ddddb -r 76fd85bbf139 src/HOLCF/Tools/pcpodef_package.ML
--- a/src/HOLCF/Tools/pcpodef_package.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/HOLCF/Tools/pcpodef_package.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -7,14 +7,14 @@
 
 signature PCPODEF_PACKAGE =
 sig
-  val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * term
-    * (string * string) option -> theory -> Proof.state
-  val pcpodef_proof_cmd: (bool * string) * (bstring * string list * mixfix) * string
-    * (string * string) option -> theory -> Proof.state
-  val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * term
-    * (string * string) option -> theory -> Proof.state
-  val cpodef_proof_cmd: (bool * string) * (bstring * string list * mixfix) * string
-    * (string * string) option -> theory -> Proof.state
+  val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
+    * (binding * binding) option -> theory -> Proof.state
+  val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
+    * (binding * binding) option -> theory -> Proof.state
+  val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
+    * (binding * binding) option -> theory -> Proof.state
+  val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
+    * (binding * binding) option -> theory -> Proof.state
 end;
 
 structure PcpodefPackage: PCPODEF_PACKAGE =
@@ -24,9 +24,6 @@
 
 (* prepare_cpodef *)
 
-fun err_in_cpodef msg name =
-  cat_error msg ("The error(s) above occurred in cpodef " ^ quote name);
-
 fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
 
 fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
@@ -36,10 +33,12 @@
   let
     val _ = Theory.requires thy "Pcpodef" "pcpodefs";
     val ctxt = ProofContext.init thy;
-    val full = Sign.full_bname thy;
+
+    val full = Sign.full_name thy;
+    val full_name = full name;
+    val bname = Binding.name_of name;
 
     (*rhs*)
-    val full_name = full name;
     val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
     val setT = Term.fastype_of set;
     val rhs_tfrees = Term.add_tfrees set [];
@@ -58,11 +57,14 @@
     val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
     val lhs_sorts = map snd lhs_tfrees;
 
-    val tname = Syntax.type_name t mx;
+    val tname = Binding.map_name (Syntax.type_name mx) t;
     val full_tname = full tname;
     val newT = Type (full_tname, map TFree lhs_tfrees);
 
-    val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
+    val (Rep_name, Abs_name) =
+      (case opt_morphs of
+        NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
+      | SOME morphs => morphs);
     val RepC = Const (full Rep_name, newT --> oldT);
     fun lessC T = Const (@{const_name sq_le}, T --> T --> HOLogic.boolT);
     val less_def = Logic.mk_equals (lessC newT,
@@ -76,7 +78,8 @@
           |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
         val less_def' = Syntax.check_term lthy3 less_def;
         val ((_, (_, less_definition')), lthy4) = lthy3
-          |> Specification.definition (NONE, ((Binding.name ("less_" ^ name ^ "_def"), []), less_def'));
+          |> Specification.definition (NONE,
+              ((Binding.prefix_name "less_" (Binding.suffix_name "_def" name), []), less_def'));
         val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
         val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
         val thy5 = lthy4
@@ -95,14 +98,14 @@
         val cpo_thms' = map (Thm.transfer theory') cpo_thms;
       in
         theory'
-        |> Sign.add_path name
+        |> Sign.add_path (Binding.name_of name)
         |> PureThy.add_thms
-          ([((Binding.name ("adm_" ^ name), admissible'), []),
-            ((Binding.name ("cont_" ^ Rep_name), @{thm typedef_cont_Rep} OF cpo_thms'), []),
-            ((Binding.name ("cont_" ^ Abs_name), @{thm typedef_cont_Abs} OF cpo_thms'), []),
-            ((Binding.name ("lub_" ^ name), @{thm typedef_lub} OF cpo_thms'), []),
-            ((Binding.name ("thelub_" ^ name), @{thm typedef_thelub} OF cpo_thms'), []),
-            ((Binding.name ("compact_" ^ name), @{thm typedef_compact} OF cpo_thms'), [])])
+          ([((Binding.prefix_name "adm_" name, admissible'), []),
+            ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
+            ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
+            ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []),
+            ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []),
+            ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])])
         |> snd
         |> Sign.parent_path
       end;
@@ -117,15 +120,14 @@
         val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
       in
         theory'
-        |> Sign.add_path name
+        |> Sign.add_path (Binding.name_of name)
         |> PureThy.add_thms
-            ([((Binding.name (Rep_name ^ "_strict"), @{thm typedef_Rep_strict} OF pcpo_thms'), []),
-              ((Binding.name (Abs_name ^ "_strict"), @{thm typedef_Abs_strict} OF pcpo_thms'), []),
-              ((Binding.name (Rep_name ^ "_strict_iff"), @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
-              ((Binding.name (Abs_name ^ "_strict_iff"), @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
-              ((Binding.name (Rep_name ^ "_defined"), @{thm typedef_Rep_defined} OF pcpo_thms'), []),
-              ((Binding.name (Abs_name ^ "_defined"), @{thm typedef_Abs_defined} OF pcpo_thms'), [])
-              ])
+          ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []),
+            ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []),
+            ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
+            ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
+            ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []),
+            ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])])
         |> snd
         |> Sign.parent_path
       end;
@@ -142,7 +144,8 @@
     then (goal_UU_mem, goal_admissible, pcpodef_result)
     else (goal_nonempty, goal_admissible, cpodef_result)
   end
-  handle ERROR msg => err_in_cpodef msg name;
+  handle ERROR msg =>
+    cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
 
 
 (* proof interface *)
@@ -174,14 +177,14 @@
 
 val typedef_proof_decl =
   Scan.optional (P.$$$ "(" |--
-      ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
+      ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
         --| P.$$$ ")") (true, NONE) --
-    (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
-    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
+    (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
+    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
 
 fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
   (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
-    ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
+    ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
 
 val _ =
   OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
diff -r 10a67c5ddddb -r 76fd85bbf139 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -245,14 +245,14 @@
   fun add_recursor thy =
       if need_recursor then
            thy |> Sign.add_consts_i
-                    [(recursor_base_name, recursor_typ, NoSyn)]
+                    [(Binding.name recursor_base_name, recursor_typ, NoSyn)]
                |> (snd o PureThy.add_defs false [(Thm.no_attributes o apfst Binding.name) recursor_def])
       else thy;
 
   val (con_defs, thy0) = thy_path
              |> Sign.add_consts_i
-                 ((case_base_name, case_typ, NoSyn) ::
-                  map #1 (List.concat con_ty_lists))
+                 (map (fn (c, T, mx) => (Binding.name c, T, mx))
+                  ((case_base_name, case_typ, NoSyn) :: map #1 (List.concat con_ty_lists)))
              |> PureThy.add_defs false
                  (map (Thm.no_attributes o apfst Binding.name)
                   (case_def ::
@@ -302,7 +302,7 @@
 
   (*** Prove the recursor theorems ***)
 
-  val recursor_eqns = case try (Thm.get_def thy1) recursor_base_name of
+  val recursor_eqns = case try (Drule.get_def thy1) recursor_base_name of
      NONE => (writeln "  [ No recursion operator ]";
               [])
    | SOME recursor_def =>
diff -r 10a67c5ddddb -r 76fd85bbf139 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -180,7 +180,7 @@
 
   (*fetch fp definitions from the theory*)
   val big_rec_def::part_rec_defs =
-    map (Thm.get_def thy1)
+    map (Drule.get_def thy1)
         (case rec_names of [_] => rec_names
                          | _   => big_rec_base_name::rec_names);
 
diff -r 10a67c5ddddb -r 76fd85bbf139 src/ZF/ind_syntax.ML
--- a/src/ZF/ind_syntax.ML	Sat Mar 07 22:16:50 2009 +0100
+++ b/src/ZF/ind_syntax.ML	Sat Mar 07 22:17:25 2009 +0100
@@ -73,7 +73,7 @@
         val T = (map (#2 o dest_Free) args) ---> iT
                 handle TERM _ => error
                     "Bad variable in constructor specification"
-        val name = Syntax.const_name id syn  (*handle infix constructors*)
+        val name = Syntax.const_name syn id
     in ((id,T,syn), name, args, prems) end;
 
 val read_constructs = map o map o read_construct;