# HG changeset patch
# User haftmann
# Date 1232552852 -3600
# Node ID b3b33e0298ebab6cb84ce8579bd8ec41eea8bdf4
# Parent  117b88da143c8a61310e0d1018ed6254be4e4fb4
binding is alias for Binding.T

diff -r 117b88da143c -r b3b33e0298eb doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Wed Jan 21 16:47:31 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Wed Jan 21 16:47:32 2009 +0100
@@ -317,7 +317,7 @@
   a theory by constant declararion and primitive definitions:
 
   \smallskip\begin{mldecls}
-  @{ML "Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix
+  @{ML "Sign.declare_const: Properties.T -> (binding * typ) * mixfix
   -> theory -> term * theory"} \\
   @{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
   \end{mldecls}
diff -r 117b88da143c -r b3b33e0298eb doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Jan 21 16:47:31 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Jan 21 16:47:32 2009 +0100
@@ -366,7 +366,7 @@
   a theory by constant declararion and primitive definitions:
 
   \smallskip\begin{mldecls}
-  \verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix|\isasep\isanewline%
+  \verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix|\isasep\isanewline%
 \verb|  -> theory -> term * theory| \\
   \verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory|
   \end{mldecls}
diff -r 117b88da143c -r b3b33e0298eb doc-src/IsarImplementation/Thy/document/logic.tex
--- a/doc-src/IsarImplementation/Thy/document/logic.tex	Wed Jan 21 16:47:31 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Wed Jan 21 16:47:32 2009 +0100
@@ -325,9 +325,9 @@
   \indexml{fastype\_of}\verb|fastype_of: term -> typ| \\
   \indexml{lambda}\verb|lambda: term -> term -> term| \\
   \indexml{betapply}\verb|betapply: term * term -> term| \\
-  \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix ->|\isasep\isanewline%
+  \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix ->|\isasep\isanewline%
 \verb|  theory -> term * theory| \\
-  \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> Binding.T * term ->|\isasep\isanewline%
+  \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> binding * term ->|\isasep\isanewline%
 \verb|  theory -> (term * term) * theory| \\
   \indexml{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
   \indexml{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
diff -r 117b88da143c -r b3b33e0298eb doc-src/IsarImplementation/Thy/document/prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Wed Jan 21 16:47:31 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Wed Jan 21 16:47:32 2009 +0100
@@ -816,13 +816,13 @@
   \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
   \indexml{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
   \indexml{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
-  \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> Binding.T -> string| \\
+  \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> binding -> string| \\
   \end{mldecls}
   \begin{mldecls}
   \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
   \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
   \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
-  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T| \\
+  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T| \\
   \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
   \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
   \end{mldecls}
diff -r 117b88da143c -r b3b33e0298eb doc-src/IsarImplementation/Thy/logic.thy
--- a/doc-src/IsarImplementation/Thy/logic.thy	Wed Jan 21 16:47:31 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/logic.thy	Wed Jan 21 16:47:32 2009 +0100
@@ -323,9 +323,9 @@
   @{index_ML fastype_of: "term -> typ"} \\
   @{index_ML lambda: "term -> term -> term"} \\
   @{index_ML betapply: "term * term -> term"} \\
-  @{index_ML Sign.declare_const: "Properties.T -> (Binding.T * typ) * mixfix ->
+  @{index_ML Sign.declare_const: "Properties.T -> (binding * typ) * mixfix ->
   theory -> term * theory"} \\
-  @{index_ML Sign.add_abbrev: "string -> Properties.T -> Binding.T * term ->
+  @{index_ML Sign.add_abbrev: "string -> Properties.T -> binding * term ->
   theory -> (term * term) * theory"} \\
   @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
   @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
diff -r 117b88da143c -r b3b33e0298eb doc-src/IsarImplementation/Thy/prelim.thy
--- a/doc-src/IsarImplementation/Thy/prelim.thy	Wed Jan 21 16:47:31 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/prelim.thy	Wed Jan 21 16:47:32 2009 +0100
@@ -707,13 +707,13 @@
   @{index_ML_type NameSpace.naming} \\
   @{index_ML NameSpace.default_naming: NameSpace.naming} \\
   @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
-  @{index_ML NameSpace.full_name: "NameSpace.naming -> Binding.T -> string"} \\
+  @{index_ML NameSpace.full_name: "NameSpace.naming -> binding -> string"} \\
   \end{mldecls}
   \begin{mldecls}
   @{index_ML_type NameSpace.T} \\
   @{index_ML NameSpace.empty: NameSpace.T} \\
   @{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\
-  @{index_ML NameSpace.declare: "NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T"} \\
+  @{index_ML NameSpace.declare: "NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T"} \\
   @{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\
   @{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\
   \end{mldecls}
diff -r 117b88da143c -r b3b33e0298eb src/HOL/Nominal/nominal_induct.ML
--- a/src/HOL/Nominal/nominal_induct.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -6,7 +6,7 @@
 
 structure NominalInduct:
 sig
-  val nominal_induct_tac: Proof.context -> (Binding.T option * term) option list list ->
+  val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
     (string * typ) list -> (string * typ) list list -> thm list ->
     thm list -> int -> RuleCases.cases_tactic
   val nominal_induct_method: Method.src -> Proof.context -> Method.method
diff -r 117b88da143c -r b3b33e0298eb src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -9,8 +9,8 @@
 signature NOMINAL_PRIMREC =
 sig
   val add_primrec: term list option -> term option ->
-    (Binding.T * typ option * mixfix) list ->
-    (Binding.T * typ option * mixfix) list ->
+    (binding * typ option * mixfix) list ->
+    (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> local_theory -> Proof.state
 end;
 
diff -r 117b88da143c -r b3b33e0298eb src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -9,14 +9,14 @@
 
 signature FUNDEF_PACKAGE =
 sig
-    val add_fundef :  (Binding.T * string option * mixfix) list
+    val add_fundef :  (binding * string option * mixfix) list
                       -> (Attrib.binding * string) list 
                       -> FundefCommon.fundef_config
                       -> bool list
                       -> local_theory
                       -> Proof.state
 
-    val add_fundef_i:  (Binding.T * typ option * mixfix) list
+    val add_fundef_i:  (binding * typ option * mixfix) list
                        -> (Attrib.binding * term) list
                        -> FundefCommon.fundef_config
                        -> bool list
diff -r 117b88da143c -r b3b33e0298eb src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -38,17 +38,17 @@
     thm list list * local_theory
   type inductive_flags
   val add_inductive_i:
-    inductive_flags -> ((Binding.T * typ) * mixfix) list ->
+    inductive_flags -> ((binding * typ) * mixfix) list ->
     (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
     inductive_result * local_theory
   val add_inductive: bool -> bool ->
-    (Binding.T * string option * mixfix) list ->
-    (Binding.T * string option * mixfix) list ->
+    (binding * string option * mixfix) list ->
+    (binding * string option * mixfix) list ->
     (Attrib.binding * string) list ->
     (Facts.ref * Attrib.src list) list ->
     bool -> local_theory -> inductive_result * local_theory
   val add_inductive_global: string -> inductive_flags ->
-    ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
+    ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
     thm list -> theory -> inductive_result * theory
   val arities_of: thm -> (string * int) list
   val params_of: thm -> term list
@@ -63,16 +63,16 @@
 sig
   include BASIC_INDUCTIVE_PACKAGE
   type add_ind_def
-  val declare_rules: string -> Binding.T -> bool -> bool -> string list ->
-    thm list -> Binding.T list -> Attrib.src list list -> (thm * string list) list ->
+  val declare_rules: string -> binding -> bool -> bool -> string list ->
+    thm list -> binding list -> Attrib.src list list -> (thm * string list) list ->
     thm -> local_theory -> thm list * thm list * thm * local_theory
   val add_ind_def: add_ind_def
   val gen_add_inductive_i: add_ind_def -> inductive_flags ->
-    ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
+    ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
     thm list -> local_theory -> inductive_result * local_theory
   val gen_add_inductive: add_ind_def -> bool -> bool ->
-    (Binding.T * string option * mixfix) list ->
-    (Binding.T * string option * mixfix) list ->
+    (binding * string option * mixfix) list ->
+    (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
     bool -> local_theory -> inductive_result * local_theory
   val gen_ind_decl: add_ind_def -> bool ->
@@ -720,13 +720,13 @@
   in (intrs', elims', induct', ctxt3) end;
 
 type inductive_flags =
-  {quiet_mode: bool, verbose: bool, kind: string, alt_name: Binding.T,
+  {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding,
    coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
 
 type add_ind_def =
   inductive_flags ->
   term list -> (Attrib.binding * term) list -> thm list ->
-  term list -> (Binding.T * mixfix) list ->
+  term list -> (binding * mixfix) list ->
   local_theory -> inductive_result * local_theory
 
 fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
diff -r 117b88da143c -r b3b33e0298eb src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -12,13 +12,13 @@
   val pred_set_conv_att: attribute
   val add_inductive_i:
     InductivePackage.inductive_flags ->
-    ((Binding.T * typ) * mixfix) list ->
+    ((binding * typ) * mixfix) list ->
     (string * typ) list ->
     (Attrib.binding * term) list -> thm list ->
     local_theory -> InductivePackage.inductive_result * local_theory
   val add_inductive: bool -> bool ->
-    (Binding.T * string option * mixfix) list ->
-    (Binding.T * string option * mixfix) list ->
+    (binding * string option * mixfix) list ->
+    (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
     bool -> local_theory -> InductivePackage.inductive_result * local_theory
   val codegen_preproc: theory -> thm list -> thm list
diff -r 117b88da143c -r b3b33e0298eb src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -7,12 +7,12 @@
 
 signature PRIMREC_PACKAGE =
 sig
-  val add_primrec: (Binding.T * typ option * mixfix) list ->
+  val add_primrec: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> local_theory -> thm list * local_theory
-  val add_primrec_global: (Binding.T * typ option * mixfix) list ->
+  val add_primrec_global: (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> thm list * theory
   val add_primrec_overloaded: (string * (string * typ) * bool) list ->
-    (Binding.T * typ option * mixfix) list ->
+    (binding * typ option * mixfix) list ->
     (Attrib.binding * term) list -> theory -> thm list * theory
 end;
 
diff -r 117b88da143c -r b3b33e0298eb src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -9,9 +9,9 @@
   val legacy_infer_term: theory -> term -> term
   val legacy_infer_prop: theory -> term -> term
   val add_fixrec: bool -> (Attrib.binding * string) list list -> theory -> theory
-  val add_fixrec_i: bool -> ((Binding.T * attribute list) * term) list list -> theory -> theory
+  val add_fixrec_i: bool -> ((binding * attribute list) * term) list list -> theory -> theory
   val add_fixpat: Attrib.binding * string list -> theory -> theory
-  val add_fixpat_i: (Binding.T * attribute list) * term list -> theory -> theory
+  val add_fixpat_i: (binding * attribute list) * term list -> theory -> theory
 end;
 
 structure FixrecPackage: FIXREC_PACKAGE =
diff -r 117b88da143c -r b3b33e0298eb src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/General/binding.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -6,6 +6,7 @@
 
 signature BASIC_BINDING =
 sig
+  type binding
   val long_names: bool ref
   val short_names: bool ref
   val unique_names: bool ref
@@ -92,6 +93,8 @@
     else space_implode "." (map mk_prefix prefix) ^ ":" ^ name
   end;
 
+type binding = T;
+
 end;
 
 structure Basic_Binding : BASIC_BINDING = Binding;
diff -r 117b88da143c -r b3b33e0298eb src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/General/name_space.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -3,9 +3,10 @@
 
 Generic name spaces with declared and hidden entries.  Unknown names
 are considered global; no support for absolute addressing.
+Cf. Pure/General/binding.ML
 *)
 
-type bstring = string;    (*names to be bound*)
+type bstring = string;    (*simple names to be bound -- legacy*)
 type xstring = string;    (*external names*)
 
 signature NAME_SPACE =
@@ -31,8 +32,8 @@
   val merge: T * T -> T
   type naming
   val default_naming: naming
-  val declare: naming -> Binding.T -> T -> string * T
-  val full_name: naming -> Binding.T -> string
+  val declare: naming -> binding -> T -> string * T
+  val full_name: naming -> binding -> string
   val external_names: naming -> string -> string list
   val path_of: naming -> string
   val add_path: string -> naming -> naming
@@ -41,7 +42,7 @@
   val sticky_prefix: string -> naming -> naming
   type 'a table = T * 'a Symtab.table
   val empty_table: 'a table
-  val bind: naming -> Binding.T * 'a
+  val bind: naming -> binding * 'a
     -> 'a table -> string * 'a table (*exception Symtab.DUP*)
   val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
   val join_tables: (string -> 'a * 'a -> 'a)
diff -r 117b88da143c -r b3b33e0298eb src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/args.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -35,7 +35,7 @@
   val name_source: T list -> string * T list
   val name_source_position: T list -> (SymbolPos.text * Position.T) * T list
   val name: T list -> string * T list
-  val binding: T list -> Binding.T * T list
+  val binding: T list -> binding * T list
   val alt_name: T list -> string * T list
   val symbol: T list -> string * T list
   val liberal_name: T list -> string * T list
@@ -66,8 +66,8 @@
   val parse1: (string -> bool) -> OuterLex.token list -> T list * OuterLex.token list
   val attribs: (string -> string) -> T list -> src list * T list
   val opt_attribs: (string -> string) -> T list -> src list * T list
-  val thm_name: (string -> string) -> string -> T list -> (Binding.T * src list) * T list
-  val opt_thm_name: (string -> string) -> string -> T list -> (Binding.T * src list) * T list
+  val thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list
+  val opt_thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list
   val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b
   val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
     src -> Proof.context -> 'a * Proof.context
diff -r 117b88da143c -r b3b33e0298eb src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -7,7 +7,7 @@
 signature ATTRIB =
 sig
   type src = Args.src
-  type binding = Binding.T * src list
+  type binding = binding * src list
   val empty_binding: binding
   val print_attributes: theory -> unit
   val intern: theory -> xstring -> string
@@ -54,7 +54,7 @@
 
 type src = Args.src;
 
-type binding = Binding.T * src list;
+type binding = binding * src list;
 val empty_binding: binding = (Binding.empty, []);
 
 
diff -r 117b88da143c -r b3b33e0298eb src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -11,10 +11,10 @@
   val mk_def: Proof.context -> (string * term) list -> term list
   val expand: cterm list -> thm -> thm
   val def_export: Assumption.export
-  val add_defs: ((Binding.T * mixfix) * ((Binding.T * attribute list) * term)) list ->
+  val add_defs: ((binding * mixfix) * ((binding * attribute list) * term)) list ->
     Proof.context -> (term * (string * thm)) list * Proof.context
-  val add_def: (Binding.T * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
-  val fixed_abbrev: (Binding.T * mixfix) * term -> Proof.context ->
+  val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
+  val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
     (term * term) * Proof.context
   val export: Proof.context -> Proof.context -> thm -> thm list * thm
   val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
diff -r 117b88da143c -r b3b33e0298eb src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -18,16 +18,16 @@
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
   val checkpoint: local_theory -> local_theory
   val full_naming: local_theory -> NameSpace.naming
-  val full_name: local_theory -> Binding.T -> string
+  val full_name: local_theory -> binding -> string
   val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val theory: (theory -> theory) -> local_theory -> local_theory
   val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
   val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   val affirm: local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
-  val abbrev: Syntax.mode -> (Binding.T * mixfix) * term -> local_theory ->
+  val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
-  val define: string -> (Binding.T * mixfix) * (Attrib.binding * term) -> local_theory ->
+  val define: string -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory
   val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
   val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
@@ -55,10 +55,10 @@
 
 type operations =
  {pretty: local_theory -> Pretty.T list,
-  abbrev: Syntax.mode -> (Binding.T * mixfix) * term -> local_theory ->
+  abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
   define: string ->
-    (Binding.T * mixfix) * (Attrib.binding * term) -> local_theory ->
+    (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
     (term * (string * thm)) * local_theory,
   notes: string ->
     (Attrib.binding * (thm list * Attrib.src list) list) list ->
diff -r 117b88da143c -r b3b33e0298eb src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/obtain.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -39,16 +39,16 @@
 signature OBTAIN =
 sig
   val thatN: string
-  val obtain: string -> (Binding.T * string option * mixfix) list ->
+  val obtain: string -> (binding * string option * mixfix) list ->
     (Attrib.binding * (string * string list) list) list ->
     bool -> Proof.state -> Proof.state
-  val obtain_i: string -> (Binding.T * typ option * mixfix) list ->
-    ((Binding.T * attribute list) * (term * term list) list) list ->
+  val obtain_i: string -> (binding * typ option * mixfix) list ->
+    ((binding * attribute list) * (term * term list) list) list ->
     bool -> Proof.state -> Proof.state
   val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
     (cterm list * thm list) * Proof.context
-  val guess: (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state
-  val guess_i: (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
+  val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
+  val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
 end;
 
 structure Obtain: OBTAIN =
diff -r 117b88da143c -r b3b33e0298eb src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -61,12 +61,12 @@
   val list: 'a parser -> 'a list parser
   val list1: 'a parser -> 'a list parser
   val name: bstring parser
-  val binding: Binding.T parser
+  val binding: binding parser
   val xname: xstring parser
   val text: string parser
   val path: Path.T parser
   val parname: string parser
-  val parbinding: Binding.T parser
+  val parbinding: binding parser
   val sort: string parser
   val arity: (string * string list * string) parser
   val multi_arity: (string list * string list * string) parser
@@ -81,11 +81,11 @@
   val opt_mixfix': mixfix parser
   val where_: string parser
   val const: (string * string * mixfix) parser
-  val params: (Binding.T * string option) list parser
-  val simple_fixes: (Binding.T * string option) list parser
-  val fixes: (Binding.T * string option * mixfix) list parser
-  val for_fixes: (Binding.T * string option * mixfix) list parser
-  val for_simple_fixes: (Binding.T * string option) list parser
+  val params: (binding * string option) list parser
+  val simple_fixes: (binding * string option) list parser
+  val fixes: (binding * string option * mixfix) list parser
+  val for_fixes: (binding * string option * mixfix) list parser
+  val for_simple_fixes: (binding * string option) list parser
   val ML_source: (SymbolPos.text * Position.T) parser
   val doc_source: (SymbolPos.text * Position.T) parser
   val term_group: string parser
diff -r 117b88da143c -r b3b33e0298eb src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -43,27 +43,27 @@
   val match_bind_i: (term list * term) list -> state -> state
   val let_bind: (string list * string) list -> state -> state
   val let_bind_i: (term list * term) list -> state -> state
-  val fix: (Binding.T * string option * mixfix) list -> state -> state
-  val fix_i: (Binding.T * typ option * mixfix) list -> state -> state
+  val fix: (binding * string option * mixfix) list -> state -> state
+  val fix_i: (binding * typ option * mixfix) list -> state -> state
   val assm: Assumption.export ->
     (Attrib.binding * (string * string list) list) list -> state -> state
   val assm_i: Assumption.export ->
-    ((Binding.T * attribute list) * (term * term list) list) list -> state -> state
+    ((binding * attribute list) * (term * term list) list) list -> state -> state
   val assume: (Attrib.binding * (string * string list) list) list -> state -> state
-  val assume_i: ((Binding.T * attribute list) * (term * term list) list) list ->
+  val assume_i: ((binding * attribute list) * (term * term list) list) list ->
     state -> state
   val presume: (Attrib.binding * (string * string list) list) list -> state -> state
-  val presume_i: ((Binding.T * attribute list) * (term * term list) list) list ->
+  val presume_i: ((binding * attribute list) * (term * term list) list) list ->
     state -> state
-  val def: (Attrib.binding * ((Binding.T * mixfix) * (string * string list))) list ->
+  val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list ->
     state -> state
-  val def_i: ((Binding.T * attribute list) *
-    ((Binding.T * mixfix) * (term * term list))) list -> state -> state
+  val def_i: ((binding * attribute list) *
+    ((binding * mixfix) * (term * term list))) list -> state -> state
   val chain: state -> state
   val chain_facts: thm list -> state -> state
   val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
   val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
-  val note_thmss_i: ((Binding.T * attribute list) *
+  val note_thmss_i: ((binding * attribute list) *
     (thm list * attribute list) list) list -> state -> state
   val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
   val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
@@ -87,7 +87,7 @@
     (theory -> 'a -> attribute) ->
     (context * 'b list -> context * (term list list * (context -> context))) ->
     string -> Method.text option -> (thm list list -> state -> state) ->
-    ((Binding.T * 'a list) * 'b) list -> state -> state
+    ((binding * 'a list) * 'b) list -> state -> state
   val local_qed: Method.text option * bool -> state -> state
   val theorem: Method.text option -> (thm list list -> context -> context) ->
     (string * string list) list list -> context -> state
@@ -107,11 +107,11 @@
   val have: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val have_i: Method.text option -> (thm list list -> state -> state) ->
-    ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
+    ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
   val show: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val show_i: Method.text option -> (thm list list -> state -> state) ->
-    ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
+    ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
   val schematic_goal: state -> bool
   val is_relevant: state -> bool
   val local_future_proof: (state -> ('a * state) Future.future) ->
diff -r 117b88da143c -r b3b33e0298eb src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -23,7 +23,7 @@
   val abbrev_mode: Proof.context -> bool
   val set_stmt: bool -> Proof.context -> Proof.context
   val naming_of: Proof.context -> NameSpace.naming
-  val full_name: Proof.context -> Binding.T -> string
+  val full_name: Proof.context -> binding -> string
   val full_bname: Proof.context -> bstring -> string
   val consts_of: Proof.context -> Consts.T
   val const_syntax_name: Proof.context -> string -> string
@@ -105,27 +105,27 @@
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val reset_naming: Proof.context -> Proof.context
   val note_thmss: string ->
-    ((Binding.T * attribute list) * (Facts.ref * attribute list) list) list ->
+    ((binding * attribute list) * (Facts.ref * attribute list) list) list ->
       Proof.context -> (string * thm list) list * Proof.context
   val note_thmss_i: string ->
-    ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
+    ((binding * attribute list) * (thm list * attribute list) list) list ->
       Proof.context -> (string * thm list) list * Proof.context
   val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
-  val read_vars: (Binding.T * string option * mixfix) list -> Proof.context ->
-    (Binding.T * typ option * mixfix) list * Proof.context
-  val cert_vars: (Binding.T * typ option * mixfix) list -> Proof.context ->
-    (Binding.T * typ option * mixfix) list * Proof.context
-  val add_fixes: (Binding.T * string option * mixfix) list ->
+  val read_vars: (binding * string option * mixfix) list -> Proof.context ->
+    (binding * typ option * mixfix) list * Proof.context
+  val cert_vars: (binding * typ option * mixfix) list -> Proof.context ->
+    (binding * typ option * mixfix) list * Proof.context
+  val add_fixes: (binding * string option * mixfix) list ->
     Proof.context -> string list * Proof.context
-  val add_fixes_i: (Binding.T * typ option * mixfix) list ->
+  val add_fixes_i: (binding * typ option * mixfix) list ->
     Proof.context -> string list * Proof.context
   val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
   val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
   val add_assms: Assumption.export ->
-    ((Binding.T * attribute list) * (string * string list) list) list ->
+    ((binding * attribute list) * (string * string list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val add_assms_i: Assumption.export ->
-    ((Binding.T * attribute list) * (term * term list) list) list ->
+    ((binding * attribute list) * (term * term list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
   val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
@@ -135,7 +135,7 @@
     Context.generic -> Context.generic
   val add_const_constraint: string * typ option -> Proof.context -> Proof.context
   val add_abbrev: string -> Properties.T ->
-    Binding.T * term -> Proof.context -> (term * term) * Proof.context
+    binding * term -> Proof.context -> (term * term) * Proof.context
   val revert_abbrev: string -> string -> Proof.context -> Proof.context
   val verbose: bool ref
   val setmp_verbose: ('a -> 'b) -> 'a -> 'b
diff -r 117b88da143c -r b3b33e0298eb src/Pure/Isar/spec_parse.ML
--- a/src/Pure/Isar/spec_parse.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/spec_parse.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -15,24 +15,23 @@
   val opt_thm_name: string -> Attrib.binding parser
   val spec: (Attrib.binding * string list) parser
   val named_spec: (Attrib.binding * string list) parser
-  val spec_name: ((Binding.T * string) * Attrib.src list) parser
-  val spec_opt_name: ((Binding.T * string) * Attrib.src list) parser
+  val spec_name: ((binding * string) * Attrib.src list) parser
+  val spec_opt_name: ((binding * string) * Attrib.src list) parser
   val xthm: (Facts.ref * Attrib.src list) parser
   val xthms1: (Facts.ref * Attrib.src list) list parser
   val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
   val locale_mixfix: mixfix parser
-  val locale_fixes: (Binding.T * string option * mixfix) list parser
+  val locale_fixes: (binding * string option * mixfix) list parser
   val locale_insts: (string option list * (Attrib.binding * string) list) parser
   val class_expr: string list parser
-  val locale_expr: Old_Locale.expr parser
-  val locale_expression: Expression.expression parser
+    val locale_expression: Expression.expression parser
   val locale_keyword: string parser
   val context_element: Element.context parser
   val statement: (Attrib.binding * (string * string list) list) list parser
   val general_statement: (Element.context list * Element.statement) parser
   val statement_keyword: string parser
   val specification:
-    (Binding.T * ((Attrib.binding * string list) list * (Binding.T * string option) list)) list parser
+    (binding * ((Attrib.binding * string list) list * (binding * string option) list)) list parser
 end;
 
 structure SpecParse: SPEC_PARSE =
@@ -115,13 +114,6 @@
 
 val class_expr = plus1_unless locale_keyword P.xname;
 
-val locale_expr =
-  let
-    fun expr2 x = (P.xname >> Old_Locale.Locale || P.$$$ "(" |-- P.!!! (expr0 --| P.$$$ ")")) x
-    and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Old_Locale.Rename || expr2) x
-    and expr0 x = (plus1_unless locale_keyword expr1 >> (fn [e] => e | es => Old_Locale.Merge es)) x;
-  in expr0 end;
-
 val locale_expression =
   let
     fun expr2 x = P.xname x;
diff -r 117b88da143c -r b3b33e0298eb src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -9,33 +9,33 @@
 signature SPECIFICATION =
 sig
   val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
-  val check_specification: (Binding.T * typ option * mixfix) list ->
+  val check_specification: (binding * typ option * mixfix) list ->
     (Attrib.binding * term list) list list -> Proof.context ->
-    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
-  val read_specification: (Binding.T * string option * mixfix) list ->
+    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+  val read_specification: (binding * string option * mixfix) list ->
     (Attrib.binding * string list) list list -> Proof.context ->
-    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
-  val check_free_specification: (Binding.T * typ option * mixfix) list ->
+    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+  val check_free_specification: (binding * typ option * mixfix) list ->
     (Attrib.binding * term list) list -> Proof.context ->
-    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
-  val read_free_specification: (Binding.T * string option * mixfix) list ->
+    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+  val read_free_specification: (binding * string option * mixfix) list ->
     (Attrib.binding * string list) list -> Proof.context ->
-    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
-  val axiomatization: (Binding.T * typ option * mixfix) list ->
+    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
+  val axiomatization: (binding * typ option * mixfix) list ->
     (Attrib.binding * term list) list -> theory ->
     (term list * (string * thm list) list) * theory
-  val axiomatization_cmd: (Binding.T * string option * mixfix) list ->
+  val axiomatization_cmd: (binding * string option * mixfix) list ->
     (Attrib.binding * string list) list -> theory ->
     (term list * (string * thm list) list) * theory
   val definition:
-    (Binding.T * typ option * mixfix) option * (Attrib.binding * term) ->
+    (binding * typ option * mixfix) option * (Attrib.binding * term) ->
     local_theory -> (term * (string * thm)) * local_theory
   val definition_cmd:
-    (Binding.T * string option * mixfix) option * (Attrib.binding * string) ->
+    (binding * string option * mixfix) option * (Attrib.binding * string) ->
     local_theory -> (term * (string * thm)) * local_theory
-  val abbreviation: Syntax.mode -> (Binding.T * typ option * mixfix) option * term ->
+  val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option * term ->
     local_theory -> local_theory
-  val abbreviation_cmd: Syntax.mode -> (Binding.T * string option * mixfix) option * string ->
+  val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string ->
     local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
@@ -149,7 +149,8 @@
 
     (*axioms*)
     val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
-        fold_map Thm.add_axiom (PureThy.name_multi (Binding.base_name b) (map subst props))
+        fold_map Thm.add_axiom
+          ((map o apfst) Binding.name (PureThy.name_multi (Binding.base_name b) (map subst props)))
         #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
     val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
       (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
diff -r 117b88da143c -r b3b33e0298eb src/Pure/consts.ML
--- a/src/Pure/consts.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/consts.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -30,10 +30,10 @@
   val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
-  val declare: bool -> NameSpace.naming -> Properties.T -> (Binding.T * typ) -> T -> T
+  val declare: bool -> NameSpace.naming -> Properties.T -> (binding * typ) -> T -> T
   val constrain: string * typ option -> T -> T
   val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
-    Binding.T * term -> T -> (term * term) * T
+    binding * term -> T -> (term * term) * T
   val revert_abbrev: string -> string -> T -> T
   val hide: bool -> string -> T -> T
   val empty: T
diff -r 117b88da143c -r b3b33e0298eb src/Pure/facts.ML
--- a/src/Pure/facts.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/facts.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -30,9 +30,9 @@
   val props: T -> thm list
   val could_unify: T -> term -> thm list
   val merge: T * T -> T
-  val add_global: NameSpace.naming -> Binding.T * thm list -> T -> string * T
-  val add_local: bool -> NameSpace.naming -> Binding.T * thm list -> T -> string * T
-  val add_dynamic: NameSpace.naming -> Binding.T * (Context.generic -> thm list) -> T -> string * T
+  val add_global: NameSpace.naming -> binding * thm list -> T -> string * T
+  val add_local: bool -> NameSpace.naming -> binding * thm list -> T -> string * T
+  val add_dynamic: NameSpace.naming -> binding * (Context.generic -> thm list) -> T -> string * T
   val del: string -> T -> T
   val hide: bool -> string -> T -> T
 end;
diff -r 117b88da143c -r b3b33e0298eb src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/morphism.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -16,21 +16,21 @@
 signature MORPHISM =
 sig
   include BASIC_MORPHISM
-  val var: morphism -> Binding.T * mixfix -> Binding.T * mixfix
-  val binding: morphism -> Binding.T -> Binding.T
+  val var: morphism -> binding * mixfix -> binding * mixfix
+  val binding: morphism -> binding -> binding
   val typ: morphism -> typ -> typ
   val term: morphism -> term -> term
   val fact: morphism -> thm list -> thm list
   val thm: morphism -> thm -> thm
   val cterm: morphism -> cterm -> cterm
   val morphism:
-   {binding: Binding.T -> Binding.T,
-    var: Binding.T * mixfix -> Binding.T * mixfix,
+   {binding: binding -> binding,
+    var: binding * mixfix -> binding * mixfix,
     typ: typ -> typ,
     term: term -> term,
     fact: thm list -> thm list} -> morphism
-  val binding_morphism: (Binding.T -> Binding.T) -> morphism
-  val var_morphism: (Binding.T * mixfix -> Binding.T * mixfix) -> morphism
+  val binding_morphism: (binding -> binding) -> morphism
+  val var_morphism: (binding * mixfix -> binding * mixfix) -> morphism
   val typ_morphism: (typ -> typ) -> morphism
   val term_morphism: (term -> term) -> morphism
   val fact_morphism: (thm list -> thm list) -> morphism
@@ -45,8 +45,8 @@
 struct
 
 datatype morphism = Morphism of
- {binding: Binding.T -> Binding.T,
-  var: Binding.T * mixfix -> Binding.T * mixfix,
+ {binding: binding -> binding,
+  var: binding * mixfix -> binding * mixfix,
   typ: typ -> typ,
   term: term -> term,
   fact: thm list -> thm list};
diff -r 117b88da143c -r b3b33e0298eb src/Pure/sign.ML
--- a/src/Pure/sign.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/sign.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -14,7 +14,7 @@
     tsig: Type.tsig,
     consts: Consts.T}
   val naming_of: theory -> NameSpace.naming
-  val full_name: theory -> Binding.T -> string
+  val full_name: theory -> binding -> string
   val base_name: string -> bstring
   val full_bname: theory -> bstring -> string
   val full_bname_path: theory -> string -> bstring -> string
@@ -91,10 +91,10 @@
   val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
   val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
-  val declare_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
+  val declare_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
   val add_consts: (bstring * string * mixfix) list -> theory -> theory
   val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
-  val add_abbrev: string -> Properties.T -> Binding.T * term -> theory -> (term * term) * theory
+  val add_abbrev: string -> Properties.T -> binding * term -> theory -> (term * term) * theory
   val revert_abbrev: string -> string -> theory -> theory
   val add_const_constraint: string * typ option -> theory -> theory
   val primitive_class: string * class list -> theory -> theory
diff -r 117b88da143c -r b3b33e0298eb src/Pure/theory.ML
--- a/src/Pure/theory.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Pure/theory.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -29,14 +29,14 @@
   val at_end: (theory -> theory option) -> theory -> theory
   val begin_theory: string -> theory list -> theory
   val end_theory: theory -> theory
+  val add_axioms_i: (binding * term) list -> theory -> theory
   val add_axioms: (bstring * string) list -> theory -> theory
-  val add_axioms_i: (bstring * term) list -> theory -> theory
   val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
+  val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
   val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory
-  val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
+  val add_finals_i: bool -> term list -> theory -> theory
   val add_finals: bool -> string list -> theory -> theory
-  val add_finals_i: bool -> term list -> theory -> theory
-  val specify_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
+  val specify_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
 end
 
 structure Theory: THEORY =
@@ -157,19 +157,19 @@
 fun err_in_axm msg name =
   cat_error msg ("The error(s) above occurred in axiom " ^ quote name);
 
-fun cert_axm thy (name, raw_tm) =
+fun cert_axm thy (b, raw_tm) =
   let
     val (t, T, _) = Sign.certify_prop thy raw_tm
       handle TYPE (msg, _, _) => error msg
         | TERM (msg, _) => error msg;
   in
     Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
-    (name, Sign.no_vars (Syntax.pp_global thy) t)
+    (b, Sign.no_vars (Syntax.pp_global thy) t)
   end;
 
-fun read_axm thy (name, str) =
-  cert_axm thy (name, Syntax.read_prop_global thy str)
-    handle ERROR msg => err_in_axm msg name;
+fun read_axm thy (bname, str) =
+  cert_axm thy (Binding.name bname, Syntax.read_prop_global thy str)
+    handle ERROR msg => err_in_axm msg bname;
 
 
 (* add_axioms(_i) *)
@@ -178,15 +178,15 @@
 
 fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
   let
-    val axms = map (apfst Binding.name o apsnd Logic.varify o prep_axm thy) raw_axms;
+    val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
     val axioms' = fold (snd oo NameSpace.bind (Sign.naming_of thy)) axms axioms
       handle Symtab.DUP dup => err_dup_axm dup;
   in axioms' end);
 
 in
 
+val add_axioms_i = gen_add_axioms cert_axm;
 val add_axioms = gen_add_axioms read_axm;
-val add_axioms_i = gen_add_axioms cert_axm;
 
 end;
 
@@ -250,16 +250,16 @@
 
 (* check_def *)
 
-fun check_def thy unchecked overloaded (bname, tm) defs =
+fun check_def thy unchecked overloaded (b, tm) defs =
   let
     val ctxt = ProofContext.init thy;
-    val name = Sign.full_bname thy bname;
+    val name = Sign.full_name thy b;
     val (lhs_const, rhs) = Sign.cert_def ctxt tm;
     val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
     val _ = check_overloading thy overloaded lhs_const;
   in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
-   [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
+   [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.display b) ^ ":"),
     Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
 
 
@@ -298,8 +298,8 @@
 
 in
 
+val add_finals_i = gen_add_finals (K I);
 val add_finals = gen_add_finals Syntax.read_term_global;
-val add_finals_i = gen_add_finals (K I);
 
 end;
 
diff -r 117b88da143c -r b3b33e0298eb src/Tools/induct.ML
--- a/src/Tools/induct.ML	Wed Jan 21 16:47:31 2009 +0100
+++ b/src/Tools/induct.ML	Wed Jan 21 16:47:32 2009 +0100
@@ -50,7 +50,7 @@
   val setN: string
   (*proof methods*)
   val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
-  val add_defs: (Binding.T option * term) option list -> Proof.context ->
+  val add_defs: (binding option * term) option list -> Proof.context ->
     (term option list * thm list) * Proof.context
   val atomize_term: theory -> term -> term
   val atomize_tac: int -> tactic
@@ -62,7 +62,7 @@
   val cases_tac: Proof.context -> term option list list -> thm option ->
     thm list -> int -> cases_tactic
   val get_inductT: Proof.context -> term option list list -> thm list list
-  val induct_tac: Proof.context -> (Binding.T option * term) option list list ->
+  val induct_tac: Proof.context -> (binding option * term) option list list ->
     (string * typ) list list -> term option list -> thm list option ->
     thm list -> int -> cases_tactic
   val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->