binding is alias for Binding.T
authorhaftmann
Wed Jan 21 16:47:32 2009 +0100 (2009-01-21)
changeset 29581b3b33e0298eb
parent 29580 117b88da143c
child 29582 0950f4f0d0cd
binding is alias for Binding.T
doc-src/IsarImplementation/Thy/ML.thy
doc-src/IsarImplementation/Thy/document/ML.tex
doc-src/IsarImplementation/Thy/document/logic.tex
doc-src/IsarImplementation/Thy/document/prelim.tex
doc-src/IsarImplementation/Thy/logic.thy
doc-src/IsarImplementation/Thy/prelim.thy
src/HOL/Nominal/nominal_induct.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_set_package.ML
src/HOL/Tools/primrec_package.ML
src/HOLCF/Tools/fixrec_package.ML
src/Pure/General/binding.ML
src/Pure/General/name_space.ML
src/Pure/Isar/args.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/spec_parse.ML
src/Pure/Isar/specification.ML
src/Pure/consts.ML
src/Pure/facts.ML
src/Pure/morphism.ML
src/Pure/sign.ML
src/Pure/theory.ML
src/Tools/induct.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Wed Jan 21 16:47:31 2009 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Wed Jan 21 16:47:32 2009 +0100
     1.3 @@ -317,7 +317,7 @@
     1.4    a theory by constant declararion and primitive definitions:
     1.5  
     1.6    \smallskip\begin{mldecls}
     1.7 -  @{ML "Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix
     1.8 +  @{ML "Sign.declare_const: Properties.T -> (binding * typ) * mixfix
     1.9    -> theory -> term * theory"} \\
    1.10    @{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
    1.11    \end{mldecls}
     2.1 --- a/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Jan 21 16:47:31 2009 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Wed Jan 21 16:47:32 2009 +0100
     2.3 @@ -366,7 +366,7 @@
     2.4    a theory by constant declararion and primitive definitions:
     2.5  
     2.6    \smallskip\begin{mldecls}
     2.7 -  \verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix|\isasep\isanewline%
     2.8 +  \verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix|\isasep\isanewline%
     2.9  \verb|  -> theory -> term * theory| \\
    2.10    \verb|Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory|
    2.11    \end{mldecls}
     3.1 --- a/doc-src/IsarImplementation/Thy/document/logic.tex	Wed Jan 21 16:47:31 2009 +0100
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Wed Jan 21 16:47:32 2009 +0100
     3.3 @@ -325,9 +325,9 @@
     3.4    \indexml{fastype\_of}\verb|fastype_of: term -> typ| \\
     3.5    \indexml{lambda}\verb|lambda: term -> term -> term| \\
     3.6    \indexml{betapply}\verb|betapply: term * term -> term| \\
     3.7 -  \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (Binding.T * typ) * mixfix ->|\isasep\isanewline%
     3.8 +  \indexml{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix ->|\isasep\isanewline%
     3.9  \verb|  theory -> term * theory| \\
    3.10 -  \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> Binding.T * term ->|\isasep\isanewline%
    3.11 +  \indexml{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> binding * term ->|\isasep\isanewline%
    3.12  \verb|  theory -> (term * term) * theory| \\
    3.13    \indexml{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
    3.14    \indexml{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
     4.1 --- a/doc-src/IsarImplementation/Thy/document/prelim.tex	Wed Jan 21 16:47:31 2009 +0100
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/prelim.tex	Wed Jan 21 16:47:32 2009 +0100
     4.3 @@ -816,13 +816,13 @@
     4.4    \indexmltype{NameSpace.naming}\verb|type NameSpace.naming| \\
     4.5    \indexml{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
     4.6    \indexml{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
     4.7 -  \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> Binding.T -> string| \\
     4.8 +  \indexml{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> binding -> string| \\
     4.9    \end{mldecls}
    4.10    \begin{mldecls}
    4.11    \indexmltype{NameSpace.T}\verb|type NameSpace.T| \\
    4.12    \indexml{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
    4.13    \indexml{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
    4.14 -  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T| \\
    4.15 +  \indexml{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T| \\
    4.16    \indexml{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
    4.17    \indexml{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
    4.18    \end{mldecls}
     5.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Wed Jan 21 16:47:31 2009 +0100
     5.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Wed Jan 21 16:47:32 2009 +0100
     5.3 @@ -323,9 +323,9 @@
     5.4    @{index_ML fastype_of: "term -> typ"} \\
     5.5    @{index_ML lambda: "term -> term -> term"} \\
     5.6    @{index_ML betapply: "term * term -> term"} \\
     5.7 -  @{index_ML Sign.declare_const: "Properties.T -> (Binding.T * typ) * mixfix ->
     5.8 +  @{index_ML Sign.declare_const: "Properties.T -> (binding * typ) * mixfix ->
     5.9    theory -> term * theory"} \\
    5.10 -  @{index_ML Sign.add_abbrev: "string -> Properties.T -> Binding.T * term ->
    5.11 +  @{index_ML Sign.add_abbrev: "string -> Properties.T -> binding * term ->
    5.12    theory -> (term * term) * theory"} \\
    5.13    @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
    5.14    @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
     6.1 --- a/doc-src/IsarImplementation/Thy/prelim.thy	Wed Jan 21 16:47:31 2009 +0100
     6.2 +++ b/doc-src/IsarImplementation/Thy/prelim.thy	Wed Jan 21 16:47:32 2009 +0100
     6.3 @@ -707,13 +707,13 @@
     6.4    @{index_ML_type NameSpace.naming} \\
     6.5    @{index_ML NameSpace.default_naming: NameSpace.naming} \\
     6.6    @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
     6.7 -  @{index_ML NameSpace.full_name: "NameSpace.naming -> Binding.T -> string"} \\
     6.8 +  @{index_ML NameSpace.full_name: "NameSpace.naming -> binding -> string"} \\
     6.9    \end{mldecls}
    6.10    \begin{mldecls}
    6.11    @{index_ML_type NameSpace.T} \\
    6.12    @{index_ML NameSpace.empty: NameSpace.T} \\
    6.13    @{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\
    6.14 -  @{index_ML NameSpace.declare: "NameSpace.naming -> Binding.T -> NameSpace.T -> string * NameSpace.T"} \\
    6.15 +  @{index_ML NameSpace.declare: "NameSpace.naming -> binding -> NameSpace.T -> string * NameSpace.T"} \\
    6.16    @{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\
    6.17    @{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\
    6.18    \end{mldecls}
     7.1 --- a/src/HOL/Nominal/nominal_induct.ML	Wed Jan 21 16:47:31 2009 +0100
     7.2 +++ b/src/HOL/Nominal/nominal_induct.ML	Wed Jan 21 16:47:32 2009 +0100
     7.3 @@ -6,7 +6,7 @@
     7.4  
     7.5  structure NominalInduct:
     7.6  sig
     7.7 -  val nominal_induct_tac: Proof.context -> (Binding.T option * term) option list list ->
     7.8 +  val nominal_induct_tac: Proof.context -> (binding option * term) option list list ->
     7.9      (string * typ) list -> (string * typ) list list -> thm list ->
    7.10      thm list -> int -> RuleCases.cases_tactic
    7.11    val nominal_induct_method: Method.src -> Proof.context -> Method.method
     8.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Wed Jan 21 16:47:31 2009 +0100
     8.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Jan 21 16:47:32 2009 +0100
     8.3 @@ -9,8 +9,8 @@
     8.4  signature NOMINAL_PRIMREC =
     8.5  sig
     8.6    val add_primrec: term list option -> term option ->
     8.7 -    (Binding.T * typ option * mixfix) list ->
     8.8 -    (Binding.T * typ option * mixfix) list ->
     8.9 +    (binding * typ option * mixfix) list ->
    8.10 +    (binding * typ option * mixfix) list ->
    8.11      (Attrib.binding * term) list -> local_theory -> Proof.state
    8.12  end;
    8.13  
     9.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Jan 21 16:47:31 2009 +0100
     9.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Jan 21 16:47:32 2009 +0100
     9.3 @@ -9,14 +9,14 @@
     9.4  
     9.5  signature FUNDEF_PACKAGE =
     9.6  sig
     9.7 -    val add_fundef :  (Binding.T * string option * mixfix) list
     9.8 +    val add_fundef :  (binding * string option * mixfix) list
     9.9                        -> (Attrib.binding * string) list 
    9.10                        -> FundefCommon.fundef_config
    9.11                        -> bool list
    9.12                        -> local_theory
    9.13                        -> Proof.state
    9.14  
    9.15 -    val add_fundef_i:  (Binding.T * typ option * mixfix) list
    9.16 +    val add_fundef_i:  (binding * typ option * mixfix) list
    9.17                         -> (Attrib.binding * term) list
    9.18                         -> FundefCommon.fundef_config
    9.19                         -> bool list
    10.1 --- a/src/HOL/Tools/inductive_package.ML	Wed Jan 21 16:47:31 2009 +0100
    10.2 +++ b/src/HOL/Tools/inductive_package.ML	Wed Jan 21 16:47:32 2009 +0100
    10.3 @@ -38,17 +38,17 @@
    10.4      thm list list * local_theory
    10.5    type inductive_flags
    10.6    val add_inductive_i:
    10.7 -    inductive_flags -> ((Binding.T * typ) * mixfix) list ->
    10.8 +    inductive_flags -> ((binding * typ) * mixfix) list ->
    10.9      (string * typ) list -> (Attrib.binding * term) list -> thm list -> local_theory ->
   10.10      inductive_result * local_theory
   10.11    val add_inductive: bool -> bool ->
   10.12 -    (Binding.T * string option * mixfix) list ->
   10.13 -    (Binding.T * string option * mixfix) list ->
   10.14 +    (binding * string option * mixfix) list ->
   10.15 +    (binding * string option * mixfix) list ->
   10.16      (Attrib.binding * string) list ->
   10.17      (Facts.ref * Attrib.src list) list ->
   10.18      bool -> local_theory -> inductive_result * local_theory
   10.19    val add_inductive_global: string -> inductive_flags ->
   10.20 -    ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
   10.21 +    ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
   10.22      thm list -> theory -> inductive_result * theory
   10.23    val arities_of: thm -> (string * int) list
   10.24    val params_of: thm -> term list
   10.25 @@ -63,16 +63,16 @@
   10.26  sig
   10.27    include BASIC_INDUCTIVE_PACKAGE
   10.28    type add_ind_def
   10.29 -  val declare_rules: string -> Binding.T -> bool -> bool -> string list ->
   10.30 -    thm list -> Binding.T list -> Attrib.src list list -> (thm * string list) list ->
   10.31 +  val declare_rules: string -> binding -> bool -> bool -> string list ->
   10.32 +    thm list -> binding list -> Attrib.src list list -> (thm * string list) list ->
   10.33      thm -> local_theory -> thm list * thm list * thm * local_theory
   10.34    val add_ind_def: add_ind_def
   10.35    val gen_add_inductive_i: add_ind_def -> inductive_flags ->
   10.36 -    ((Binding.T * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
   10.37 +    ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
   10.38      thm list -> local_theory -> inductive_result * local_theory
   10.39    val gen_add_inductive: add_ind_def -> bool -> bool ->
   10.40 -    (Binding.T * string option * mixfix) list ->
   10.41 -    (Binding.T * string option * mixfix) list ->
   10.42 +    (binding * string option * mixfix) list ->
   10.43 +    (binding * string option * mixfix) list ->
   10.44      (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
   10.45      bool -> local_theory -> inductive_result * local_theory
   10.46    val gen_ind_decl: add_ind_def -> bool ->
   10.47 @@ -720,13 +720,13 @@
   10.48    in (intrs', elims', induct', ctxt3) end;
   10.49  
   10.50  type inductive_flags =
   10.51 -  {quiet_mode: bool, verbose: bool, kind: string, alt_name: Binding.T,
   10.52 +  {quiet_mode: bool, verbose: bool, kind: string, alt_name: binding,
   10.53     coind: bool, no_elim: bool, no_ind: bool, skip_mono: bool, fork_mono: bool}
   10.54  
   10.55  type add_ind_def =
   10.56    inductive_flags ->
   10.57    term list -> (Attrib.binding * term) list -> thm list ->
   10.58 -  term list -> (Binding.T * mixfix) list ->
   10.59 +  term list -> (binding * mixfix) list ->
   10.60    local_theory -> inductive_result * local_theory
   10.61  
   10.62  fun add_ind_def {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
    11.1 --- a/src/HOL/Tools/inductive_set_package.ML	Wed Jan 21 16:47:31 2009 +0100
    11.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Wed Jan 21 16:47:32 2009 +0100
    11.3 @@ -12,13 +12,13 @@
    11.4    val pred_set_conv_att: attribute
    11.5    val add_inductive_i:
    11.6      InductivePackage.inductive_flags ->
    11.7 -    ((Binding.T * typ) * mixfix) list ->
    11.8 +    ((binding * typ) * mixfix) list ->
    11.9      (string * typ) list ->
   11.10      (Attrib.binding * term) list -> thm list ->
   11.11      local_theory -> InductivePackage.inductive_result * local_theory
   11.12    val add_inductive: bool -> bool ->
   11.13 -    (Binding.T * string option * mixfix) list ->
   11.14 -    (Binding.T * string option * mixfix) list ->
   11.15 +    (binding * string option * mixfix) list ->
   11.16 +    (binding * string option * mixfix) list ->
   11.17      (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
   11.18      bool -> local_theory -> InductivePackage.inductive_result * local_theory
   11.19    val codegen_preproc: theory -> thm list -> thm list
    12.1 --- a/src/HOL/Tools/primrec_package.ML	Wed Jan 21 16:47:31 2009 +0100
    12.2 +++ b/src/HOL/Tools/primrec_package.ML	Wed Jan 21 16:47:32 2009 +0100
    12.3 @@ -7,12 +7,12 @@
    12.4  
    12.5  signature PRIMREC_PACKAGE =
    12.6  sig
    12.7 -  val add_primrec: (Binding.T * typ option * mixfix) list ->
    12.8 +  val add_primrec: (binding * typ option * mixfix) list ->
    12.9      (Attrib.binding * term) list -> local_theory -> thm list * local_theory
   12.10 -  val add_primrec_global: (Binding.T * typ option * mixfix) list ->
   12.11 +  val add_primrec_global: (binding * typ option * mixfix) list ->
   12.12      (Attrib.binding * term) list -> theory -> thm list * theory
   12.13    val add_primrec_overloaded: (string * (string * typ) * bool) list ->
   12.14 -    (Binding.T * typ option * mixfix) list ->
   12.15 +    (binding * typ option * mixfix) list ->
   12.16      (Attrib.binding * term) list -> theory -> thm list * theory
   12.17  end;
   12.18  
    13.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Wed Jan 21 16:47:31 2009 +0100
    13.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Wed Jan 21 16:47:32 2009 +0100
    13.3 @@ -9,9 +9,9 @@
    13.4    val legacy_infer_term: theory -> term -> term
    13.5    val legacy_infer_prop: theory -> term -> term
    13.6    val add_fixrec: bool -> (Attrib.binding * string) list list -> theory -> theory
    13.7 -  val add_fixrec_i: bool -> ((Binding.T * attribute list) * term) list list -> theory -> theory
    13.8 +  val add_fixrec_i: bool -> ((binding * attribute list) * term) list list -> theory -> theory
    13.9    val add_fixpat: Attrib.binding * string list -> theory -> theory
   13.10 -  val add_fixpat_i: (Binding.T * attribute list) * term list -> theory -> theory
   13.11 +  val add_fixpat_i: (binding * attribute list) * term list -> theory -> theory
   13.12  end;
   13.13  
   13.14  structure FixrecPackage: FIXREC_PACKAGE =
    14.1 --- a/src/Pure/General/binding.ML	Wed Jan 21 16:47:31 2009 +0100
    14.2 +++ b/src/Pure/General/binding.ML	Wed Jan 21 16:47:32 2009 +0100
    14.3 @@ -6,6 +6,7 @@
    14.4  
    14.5  signature BASIC_BINDING =
    14.6  sig
    14.7 +  type binding
    14.8    val long_names: bool ref
    14.9    val short_names: bool ref
   14.10    val unique_names: bool ref
   14.11 @@ -92,6 +93,8 @@
   14.12      else space_implode "." (map mk_prefix prefix) ^ ":" ^ name
   14.13    end;
   14.14  
   14.15 +type binding = T;
   14.16 +
   14.17  end;
   14.18  
   14.19  structure Basic_Binding : BASIC_BINDING = Binding;
    15.1 --- a/src/Pure/General/name_space.ML	Wed Jan 21 16:47:31 2009 +0100
    15.2 +++ b/src/Pure/General/name_space.ML	Wed Jan 21 16:47:32 2009 +0100
    15.3 @@ -3,9 +3,10 @@
    15.4  
    15.5  Generic name spaces with declared and hidden entries.  Unknown names
    15.6  are considered global; no support for absolute addressing.
    15.7 +Cf. Pure/General/binding.ML
    15.8  *)
    15.9  
   15.10 -type bstring = string;    (*names to be bound*)
   15.11 +type bstring = string;    (*simple names to be bound -- legacy*)
   15.12  type xstring = string;    (*external names*)
   15.13  
   15.14  signature NAME_SPACE =
   15.15 @@ -31,8 +32,8 @@
   15.16    val merge: T * T -> T
   15.17    type naming
   15.18    val default_naming: naming
   15.19 -  val declare: naming -> Binding.T -> T -> string * T
   15.20 -  val full_name: naming -> Binding.T -> string
   15.21 +  val declare: naming -> binding -> T -> string * T
   15.22 +  val full_name: naming -> binding -> string
   15.23    val external_names: naming -> string -> string list
   15.24    val path_of: naming -> string
   15.25    val add_path: string -> naming -> naming
   15.26 @@ -41,7 +42,7 @@
   15.27    val sticky_prefix: string -> naming -> naming
   15.28    type 'a table = T * 'a Symtab.table
   15.29    val empty_table: 'a table
   15.30 -  val bind: naming -> Binding.T * 'a
   15.31 +  val bind: naming -> binding * 'a
   15.32      -> 'a table -> string * 'a table (*exception Symtab.DUP*)
   15.33    val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
   15.34    val join_tables: (string -> 'a * 'a -> 'a)
    16.1 --- a/src/Pure/Isar/args.ML	Wed Jan 21 16:47:31 2009 +0100
    16.2 +++ b/src/Pure/Isar/args.ML	Wed Jan 21 16:47:32 2009 +0100
    16.3 @@ -35,7 +35,7 @@
    16.4    val name_source: T list -> string * T list
    16.5    val name_source_position: T list -> (SymbolPos.text * Position.T) * T list
    16.6    val name: T list -> string * T list
    16.7 -  val binding: T list -> Binding.T * T list
    16.8 +  val binding: T list -> binding * T list
    16.9    val alt_name: T list -> string * T list
   16.10    val symbol: T list -> string * T list
   16.11    val liberal_name: T list -> string * T list
   16.12 @@ -66,8 +66,8 @@
   16.13    val parse1: (string -> bool) -> OuterLex.token list -> T list * OuterLex.token list
   16.14    val attribs: (string -> string) -> T list -> src list * T list
   16.15    val opt_attribs: (string -> string) -> T list -> src list * T list
   16.16 -  val thm_name: (string -> string) -> string -> T list -> (Binding.T * src list) * T list
   16.17 -  val opt_thm_name: (string -> string) -> string -> T list -> (Binding.T * src list) * T list
   16.18 +  val thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list
   16.19 +  val opt_thm_name: (string -> string) -> string -> T list -> (binding * src list) * T list
   16.20    val syntax: string -> ('b * T list -> 'a * ('b * T list)) -> src -> 'b -> 'a * 'b
   16.21    val context_syntax: string -> (Context.generic * T list -> 'a * (Context.generic * T list)) ->
   16.22      src -> Proof.context -> 'a * Proof.context
    17.1 --- a/src/Pure/Isar/attrib.ML	Wed Jan 21 16:47:31 2009 +0100
    17.2 +++ b/src/Pure/Isar/attrib.ML	Wed Jan 21 16:47:32 2009 +0100
    17.3 @@ -7,7 +7,7 @@
    17.4  signature ATTRIB =
    17.5  sig
    17.6    type src = Args.src
    17.7 -  type binding = Binding.T * src list
    17.8 +  type binding = binding * src list
    17.9    val empty_binding: binding
   17.10    val print_attributes: theory -> unit
   17.11    val intern: theory -> xstring -> string
   17.12 @@ -54,7 +54,7 @@
   17.13  
   17.14  type src = Args.src;
   17.15  
   17.16 -type binding = Binding.T * src list;
   17.17 +type binding = binding * src list;
   17.18  val empty_binding: binding = (Binding.empty, []);
   17.19  
   17.20  
    18.1 --- a/src/Pure/Isar/local_defs.ML	Wed Jan 21 16:47:31 2009 +0100
    18.2 +++ b/src/Pure/Isar/local_defs.ML	Wed Jan 21 16:47:32 2009 +0100
    18.3 @@ -11,10 +11,10 @@
    18.4    val mk_def: Proof.context -> (string * term) list -> term list
    18.5    val expand: cterm list -> thm -> thm
    18.6    val def_export: Assumption.export
    18.7 -  val add_defs: ((Binding.T * mixfix) * ((Binding.T * attribute list) * term)) list ->
    18.8 +  val add_defs: ((binding * mixfix) * ((binding * attribute list) * term)) list ->
    18.9      Proof.context -> (term * (string * thm)) list * Proof.context
   18.10 -  val add_def: (Binding.T * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
   18.11 -  val fixed_abbrev: (Binding.T * mixfix) * term -> Proof.context ->
   18.12 +  val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
   18.13 +  val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
   18.14      (term * term) * Proof.context
   18.15    val export: Proof.context -> Proof.context -> thm -> thm list * thm
   18.16    val export_cterm: Proof.context -> Proof.context -> cterm -> cterm * thm
    19.1 --- a/src/Pure/Isar/local_theory.ML	Wed Jan 21 16:47:31 2009 +0100
    19.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Jan 21 16:47:32 2009 +0100
    19.3 @@ -18,16 +18,16 @@
    19.4    val raw_theory: (theory -> theory) -> local_theory -> local_theory
    19.5    val checkpoint: local_theory -> local_theory
    19.6    val full_naming: local_theory -> NameSpace.naming
    19.7 -  val full_name: local_theory -> Binding.T -> string
    19.8 +  val full_name: local_theory -> binding -> string
    19.9    val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   19.10    val theory: (theory -> theory) -> local_theory -> local_theory
   19.11    val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
   19.12    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
   19.13    val affirm: local_theory -> local_theory
   19.14    val pretty: local_theory -> Pretty.T list
   19.15 -  val abbrev: Syntax.mode -> (Binding.T * mixfix) * term -> local_theory ->
   19.16 +  val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
   19.17      (term * term) * local_theory
   19.18 -  val define: string -> (Binding.T * mixfix) * (Attrib.binding * term) -> local_theory ->
   19.19 +  val define: string -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
   19.20      (term * (string * thm)) * local_theory
   19.21    val note: string -> Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
   19.22    val notes: string -> (Attrib.binding * (thm list * Attrib.src list) list) list ->
   19.23 @@ -55,10 +55,10 @@
   19.24  
   19.25  type operations =
   19.26   {pretty: local_theory -> Pretty.T list,
   19.27 -  abbrev: Syntax.mode -> (Binding.T * mixfix) * term -> local_theory ->
   19.28 +  abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
   19.29      (term * term) * local_theory,
   19.30    define: string ->
   19.31 -    (Binding.T * mixfix) * (Attrib.binding * term) -> local_theory ->
   19.32 +    (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
   19.33      (term * (string * thm)) * local_theory,
   19.34    notes: string ->
   19.35      (Attrib.binding * (thm list * Attrib.src list) list) list ->
    20.1 --- a/src/Pure/Isar/obtain.ML	Wed Jan 21 16:47:31 2009 +0100
    20.2 +++ b/src/Pure/Isar/obtain.ML	Wed Jan 21 16:47:32 2009 +0100
    20.3 @@ -39,16 +39,16 @@
    20.4  signature OBTAIN =
    20.5  sig
    20.6    val thatN: string
    20.7 -  val obtain: string -> (Binding.T * string option * mixfix) list ->
    20.8 +  val obtain: string -> (binding * string option * mixfix) list ->
    20.9      (Attrib.binding * (string * string list) list) list ->
   20.10      bool -> Proof.state -> Proof.state
   20.11 -  val obtain_i: string -> (Binding.T * typ option * mixfix) list ->
   20.12 -    ((Binding.T * attribute list) * (term * term list) list) list ->
   20.13 +  val obtain_i: string -> (binding * typ option * mixfix) list ->
   20.14 +    ((binding * attribute list) * (term * term list) list) list ->
   20.15      bool -> Proof.state -> Proof.state
   20.16    val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
   20.17      (cterm list * thm list) * Proof.context
   20.18 -  val guess: (Binding.T * string option * mixfix) list -> bool -> Proof.state -> Proof.state
   20.19 -  val guess_i: (Binding.T * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
   20.20 +  val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
   20.21 +  val guess_i: (binding * typ option * mixfix) list -> bool -> Proof.state -> Proof.state
   20.22  end;
   20.23  
   20.24  structure Obtain: OBTAIN =
    21.1 --- a/src/Pure/Isar/outer_parse.ML	Wed Jan 21 16:47:31 2009 +0100
    21.2 +++ b/src/Pure/Isar/outer_parse.ML	Wed Jan 21 16:47:32 2009 +0100
    21.3 @@ -61,12 +61,12 @@
    21.4    val list: 'a parser -> 'a list parser
    21.5    val list1: 'a parser -> 'a list parser
    21.6    val name: bstring parser
    21.7 -  val binding: Binding.T parser
    21.8 +  val binding: binding parser
    21.9    val xname: xstring parser
   21.10    val text: string parser
   21.11    val path: Path.T parser
   21.12    val parname: string parser
   21.13 -  val parbinding: Binding.T parser
   21.14 +  val parbinding: binding parser
   21.15    val sort: string parser
   21.16    val arity: (string * string list * string) parser
   21.17    val multi_arity: (string list * string list * string) parser
   21.18 @@ -81,11 +81,11 @@
   21.19    val opt_mixfix': mixfix parser
   21.20    val where_: string parser
   21.21    val const: (string * string * mixfix) parser
   21.22 -  val params: (Binding.T * string option) list parser
   21.23 -  val simple_fixes: (Binding.T * string option) list parser
   21.24 -  val fixes: (Binding.T * string option * mixfix) list parser
   21.25 -  val for_fixes: (Binding.T * string option * mixfix) list parser
   21.26 -  val for_simple_fixes: (Binding.T * string option) list parser
   21.27 +  val params: (binding * string option) list parser
   21.28 +  val simple_fixes: (binding * string option) list parser
   21.29 +  val fixes: (binding * string option * mixfix) list parser
   21.30 +  val for_fixes: (binding * string option * mixfix) list parser
   21.31 +  val for_simple_fixes: (binding * string option) list parser
   21.32    val ML_source: (SymbolPos.text * Position.T) parser
   21.33    val doc_source: (SymbolPos.text * Position.T) parser
   21.34    val term_group: string parser
    22.1 --- a/src/Pure/Isar/proof.ML	Wed Jan 21 16:47:31 2009 +0100
    22.2 +++ b/src/Pure/Isar/proof.ML	Wed Jan 21 16:47:32 2009 +0100
    22.3 @@ -43,27 +43,27 @@
    22.4    val match_bind_i: (term list * term) list -> state -> state
    22.5    val let_bind: (string list * string) list -> state -> state
    22.6    val let_bind_i: (term list * term) list -> state -> state
    22.7 -  val fix: (Binding.T * string option * mixfix) list -> state -> state
    22.8 -  val fix_i: (Binding.T * typ option * mixfix) list -> state -> state
    22.9 +  val fix: (binding * string option * mixfix) list -> state -> state
   22.10 +  val fix_i: (binding * typ option * mixfix) list -> state -> state
   22.11    val assm: Assumption.export ->
   22.12      (Attrib.binding * (string * string list) list) list -> state -> state
   22.13    val assm_i: Assumption.export ->
   22.14 -    ((Binding.T * attribute list) * (term * term list) list) list -> state -> state
   22.15 +    ((binding * attribute list) * (term * term list) list) list -> state -> state
   22.16    val assume: (Attrib.binding * (string * string list) list) list -> state -> state
   22.17 -  val assume_i: ((Binding.T * attribute list) * (term * term list) list) list ->
   22.18 +  val assume_i: ((binding * attribute list) * (term * term list) list) list ->
   22.19      state -> state
   22.20    val presume: (Attrib.binding * (string * string list) list) list -> state -> state
   22.21 -  val presume_i: ((Binding.T * attribute list) * (term * term list) list) list ->
   22.22 +  val presume_i: ((binding * attribute list) * (term * term list) list) list ->
   22.23      state -> state
   22.24 -  val def: (Attrib.binding * ((Binding.T * mixfix) * (string * string list))) list ->
   22.25 +  val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list ->
   22.26      state -> state
   22.27 -  val def_i: ((Binding.T * attribute list) *
   22.28 -    ((Binding.T * mixfix) * (term * term list))) list -> state -> state
   22.29 +  val def_i: ((binding * attribute list) *
   22.30 +    ((binding * mixfix) * (term * term list))) list -> state -> state
   22.31    val chain: state -> state
   22.32    val chain_facts: thm list -> state -> state
   22.33    val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
   22.34    val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
   22.35 -  val note_thmss_i: ((Binding.T * attribute list) *
   22.36 +  val note_thmss_i: ((binding * attribute list) *
   22.37      (thm list * attribute list) list) list -> state -> state
   22.38    val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
   22.39    val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
   22.40 @@ -87,7 +87,7 @@
   22.41      (theory -> 'a -> attribute) ->
   22.42      (context * 'b list -> context * (term list list * (context -> context))) ->
   22.43      string -> Method.text option -> (thm list list -> state -> state) ->
   22.44 -    ((Binding.T * 'a list) * 'b) list -> state -> state
   22.45 +    ((binding * 'a list) * 'b) list -> state -> state
   22.46    val local_qed: Method.text option * bool -> state -> state
   22.47    val theorem: Method.text option -> (thm list list -> context -> context) ->
   22.48      (string * string list) list list -> context -> state
   22.49 @@ -107,11 +107,11 @@
   22.50    val have: Method.text option -> (thm list list -> state -> state) ->
   22.51      (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   22.52    val have_i: Method.text option -> (thm list list -> state -> state) ->
   22.53 -    ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
   22.54 +    ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
   22.55    val show: Method.text option -> (thm list list -> state -> state) ->
   22.56      (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   22.57    val show_i: Method.text option -> (thm list list -> state -> state) ->
   22.58 -    ((Binding.T * attribute list) * (term * term list) list) list -> bool -> state -> state
   22.59 +    ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
   22.60    val schematic_goal: state -> bool
   22.61    val is_relevant: state -> bool
   22.62    val local_future_proof: (state -> ('a * state) Future.future) ->
    23.1 --- a/src/Pure/Isar/proof_context.ML	Wed Jan 21 16:47:31 2009 +0100
    23.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Jan 21 16:47:32 2009 +0100
    23.3 @@ -23,7 +23,7 @@
    23.4    val abbrev_mode: Proof.context -> bool
    23.5    val set_stmt: bool -> Proof.context -> Proof.context
    23.6    val naming_of: Proof.context -> NameSpace.naming
    23.7 -  val full_name: Proof.context -> Binding.T -> string
    23.8 +  val full_name: Proof.context -> binding -> string
    23.9    val full_bname: Proof.context -> bstring -> string
   23.10    val consts_of: Proof.context -> Consts.T
   23.11    val const_syntax_name: Proof.context -> string -> string
   23.12 @@ -105,27 +105,27 @@
   23.13    val restore_naming: Proof.context -> Proof.context -> Proof.context
   23.14    val reset_naming: Proof.context -> Proof.context
   23.15    val note_thmss: string ->
   23.16 -    ((Binding.T * attribute list) * (Facts.ref * attribute list) list) list ->
   23.17 +    ((binding * attribute list) * (Facts.ref * attribute list) list) list ->
   23.18        Proof.context -> (string * thm list) list * Proof.context
   23.19    val note_thmss_i: string ->
   23.20 -    ((Binding.T * attribute list) * (thm list * attribute list) list) list ->
   23.21 +    ((binding * attribute list) * (thm list * attribute list) list) list ->
   23.22        Proof.context -> (string * thm list) list * Proof.context
   23.23    val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
   23.24 -  val read_vars: (Binding.T * string option * mixfix) list -> Proof.context ->
   23.25 -    (Binding.T * typ option * mixfix) list * Proof.context
   23.26 -  val cert_vars: (Binding.T * typ option * mixfix) list -> Proof.context ->
   23.27 -    (Binding.T * typ option * mixfix) list * Proof.context
   23.28 -  val add_fixes: (Binding.T * string option * mixfix) list ->
   23.29 +  val read_vars: (binding * string option * mixfix) list -> Proof.context ->
   23.30 +    (binding * typ option * mixfix) list * Proof.context
   23.31 +  val cert_vars: (binding * typ option * mixfix) list -> Proof.context ->
   23.32 +    (binding * typ option * mixfix) list * Proof.context
   23.33 +  val add_fixes: (binding * string option * mixfix) list ->
   23.34      Proof.context -> string list * Proof.context
   23.35 -  val add_fixes_i: (Binding.T * typ option * mixfix) list ->
   23.36 +  val add_fixes_i: (binding * typ option * mixfix) list ->
   23.37      Proof.context -> string list * Proof.context
   23.38    val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
   23.39    val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
   23.40    val add_assms: Assumption.export ->
   23.41 -    ((Binding.T * attribute list) * (string * string list) list) list ->
   23.42 +    ((binding * attribute list) * (string * string list) list) list ->
   23.43      Proof.context -> (string * thm list) list * Proof.context
   23.44    val add_assms_i: Assumption.export ->
   23.45 -    ((Binding.T * attribute list) * (term * term list) list) list ->
   23.46 +    ((binding * attribute list) * (term * term list) list) list ->
   23.47      Proof.context -> (string * thm list) list * Proof.context
   23.48    val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
   23.49    val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
   23.50 @@ -135,7 +135,7 @@
   23.51      Context.generic -> Context.generic
   23.52    val add_const_constraint: string * typ option -> Proof.context -> Proof.context
   23.53    val add_abbrev: string -> Properties.T ->
   23.54 -    Binding.T * term -> Proof.context -> (term * term) * Proof.context
   23.55 +    binding * term -> Proof.context -> (term * term) * Proof.context
   23.56    val revert_abbrev: string -> string -> Proof.context -> Proof.context
   23.57    val verbose: bool ref
   23.58    val setmp_verbose: ('a -> 'b) -> 'a -> 'b
    24.1 --- a/src/Pure/Isar/spec_parse.ML	Wed Jan 21 16:47:31 2009 +0100
    24.2 +++ b/src/Pure/Isar/spec_parse.ML	Wed Jan 21 16:47:32 2009 +0100
    24.3 @@ -15,24 +15,23 @@
    24.4    val opt_thm_name: string -> Attrib.binding parser
    24.5    val spec: (Attrib.binding * string list) parser
    24.6    val named_spec: (Attrib.binding * string list) parser
    24.7 -  val spec_name: ((Binding.T * string) * Attrib.src list) parser
    24.8 -  val spec_opt_name: ((Binding.T * string) * Attrib.src list) parser
    24.9 +  val spec_name: ((binding * string) * Attrib.src list) parser
   24.10 +  val spec_opt_name: ((binding * string) * Attrib.src list) parser
   24.11    val xthm: (Facts.ref * Attrib.src list) parser
   24.12    val xthms1: (Facts.ref * Attrib.src list) list parser
   24.13    val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
   24.14    val locale_mixfix: mixfix parser
   24.15 -  val locale_fixes: (Binding.T * string option * mixfix) list parser
   24.16 +  val locale_fixes: (binding * string option * mixfix) list parser
   24.17    val locale_insts: (string option list * (Attrib.binding * string) list) parser
   24.18    val class_expr: string list parser
   24.19 -  val locale_expr: Old_Locale.expr parser
   24.20 -  val locale_expression: Expression.expression parser
   24.21 +    val locale_expression: Expression.expression parser
   24.22    val locale_keyword: string parser
   24.23    val context_element: Element.context parser
   24.24    val statement: (Attrib.binding * (string * string list) list) list parser
   24.25    val general_statement: (Element.context list * Element.statement) parser
   24.26    val statement_keyword: string parser
   24.27    val specification:
   24.28 -    (Binding.T * ((Attrib.binding * string list) list * (Binding.T * string option) list)) list parser
   24.29 +    (binding * ((Attrib.binding * string list) list * (binding * string option) list)) list parser
   24.30  end;
   24.31  
   24.32  structure SpecParse: SPEC_PARSE =
   24.33 @@ -115,13 +114,6 @@
   24.34  
   24.35  val class_expr = plus1_unless locale_keyword P.xname;
   24.36  
   24.37 -val locale_expr =
   24.38 -  let
   24.39 -    fun expr2 x = (P.xname >> Old_Locale.Locale || P.$$$ "(" |-- P.!!! (expr0 --| P.$$$ ")")) x
   24.40 -    and expr1 x = (expr2 -- Scan.repeat1 (P.maybe rename) >> Old_Locale.Rename || expr2) x
   24.41 -    and expr0 x = (plus1_unless locale_keyword expr1 >> (fn [e] => e | es => Old_Locale.Merge es)) x;
   24.42 -  in expr0 end;
   24.43 -
   24.44  val locale_expression =
   24.45    let
   24.46      fun expr2 x = P.xname x;
    25.1 --- a/src/Pure/Isar/specification.ML	Wed Jan 21 16:47:31 2009 +0100
    25.2 +++ b/src/Pure/Isar/specification.ML	Wed Jan 21 16:47:32 2009 +0100
    25.3 @@ -9,33 +9,33 @@
    25.4  signature SPECIFICATION =
    25.5  sig
    25.6    val print_consts: local_theory -> (string * typ -> bool) -> (string * typ) list -> unit
    25.7 -  val check_specification: (Binding.T * typ option * mixfix) list ->
    25.8 +  val check_specification: (binding * typ option * mixfix) list ->
    25.9      (Attrib.binding * term list) list list -> Proof.context ->
   25.10 -    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   25.11 -  val read_specification: (Binding.T * string option * mixfix) list ->
   25.12 +    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   25.13 +  val read_specification: (binding * string option * mixfix) list ->
   25.14      (Attrib.binding * string list) list list -> Proof.context ->
   25.15 -    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   25.16 -  val check_free_specification: (Binding.T * typ option * mixfix) list ->
   25.17 +    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   25.18 +  val check_free_specification: (binding * typ option * mixfix) list ->
   25.19      (Attrib.binding * term list) list -> Proof.context ->
   25.20 -    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   25.21 -  val read_free_specification: (Binding.T * string option * mixfix) list ->
   25.22 +    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   25.23 +  val read_free_specification: (binding * string option * mixfix) list ->
   25.24      (Attrib.binding * string list) list -> Proof.context ->
   25.25 -    (((Binding.T * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   25.26 -  val axiomatization: (Binding.T * typ option * mixfix) list ->
   25.27 +    (((binding * typ) * mixfix) list * (Attrib.binding * term list) list) * Proof.context
   25.28 +  val axiomatization: (binding * typ option * mixfix) list ->
   25.29      (Attrib.binding * term list) list -> theory ->
   25.30      (term list * (string * thm list) list) * theory
   25.31 -  val axiomatization_cmd: (Binding.T * string option * mixfix) list ->
   25.32 +  val axiomatization_cmd: (binding * string option * mixfix) list ->
   25.33      (Attrib.binding * string list) list -> theory ->
   25.34      (term list * (string * thm list) list) * theory
   25.35    val definition:
   25.36 -    (Binding.T * typ option * mixfix) option * (Attrib.binding * term) ->
   25.37 +    (binding * typ option * mixfix) option * (Attrib.binding * term) ->
   25.38      local_theory -> (term * (string * thm)) * local_theory
   25.39    val definition_cmd:
   25.40 -    (Binding.T * string option * mixfix) option * (Attrib.binding * string) ->
   25.41 +    (binding * string option * mixfix) option * (Attrib.binding * string) ->
   25.42      local_theory -> (term * (string * thm)) * local_theory
   25.43 -  val abbreviation: Syntax.mode -> (Binding.T * typ option * mixfix) option * term ->
   25.44 +  val abbreviation: Syntax.mode -> (binding * typ option * mixfix) option * term ->
   25.45      local_theory -> local_theory
   25.46 -  val abbreviation_cmd: Syntax.mode -> (Binding.T * string option * mixfix) option * string ->
   25.47 +  val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string ->
   25.48      local_theory -> local_theory
   25.49    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   25.50    val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   25.51 @@ -149,7 +149,8 @@
   25.52  
   25.53      (*axioms*)
   25.54      val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
   25.55 -        fold_map Thm.add_axiom (PureThy.name_multi (Binding.base_name b) (map subst props))
   25.56 +        fold_map Thm.add_axiom
   25.57 +          ((map o apfst) Binding.name (PureThy.name_multi (Binding.base_name b) (map subst props)))
   25.58          #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
   25.59      val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
   25.60        (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
    26.1 --- a/src/Pure/consts.ML	Wed Jan 21 16:47:31 2009 +0100
    26.2 +++ b/src/Pure/consts.ML	Wed Jan 21 16:47:32 2009 +0100
    26.3 @@ -30,10 +30,10 @@
    26.4    val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
    26.5    val typargs: T -> string * typ -> typ list
    26.6    val instance: T -> string * typ list -> typ
    26.7 -  val declare: bool -> NameSpace.naming -> Properties.T -> (Binding.T * typ) -> T -> T
    26.8 +  val declare: bool -> NameSpace.naming -> Properties.T -> (binding * typ) -> T -> T
    26.9    val constrain: string * typ option -> T -> T
   26.10    val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
   26.11 -    Binding.T * term -> T -> (term * term) * T
   26.12 +    binding * term -> T -> (term * term) * T
   26.13    val revert_abbrev: string -> string -> T -> T
   26.14    val hide: bool -> string -> T -> T
   26.15    val empty: T
    27.1 --- a/src/Pure/facts.ML	Wed Jan 21 16:47:31 2009 +0100
    27.2 +++ b/src/Pure/facts.ML	Wed Jan 21 16:47:32 2009 +0100
    27.3 @@ -30,9 +30,9 @@
    27.4    val props: T -> thm list
    27.5    val could_unify: T -> term -> thm list
    27.6    val merge: T * T -> T
    27.7 -  val add_global: NameSpace.naming -> Binding.T * thm list -> T -> string * T
    27.8 -  val add_local: bool -> NameSpace.naming -> Binding.T * thm list -> T -> string * T
    27.9 -  val add_dynamic: NameSpace.naming -> Binding.T * (Context.generic -> thm list) -> T -> string * T
   27.10 +  val add_global: NameSpace.naming -> binding * thm list -> T -> string * T
   27.11 +  val add_local: bool -> NameSpace.naming -> binding * thm list -> T -> string * T
   27.12 +  val add_dynamic: NameSpace.naming -> binding * (Context.generic -> thm list) -> T -> string * T
   27.13    val del: string -> T -> T
   27.14    val hide: bool -> string -> T -> T
   27.15  end;
    28.1 --- a/src/Pure/morphism.ML	Wed Jan 21 16:47:31 2009 +0100
    28.2 +++ b/src/Pure/morphism.ML	Wed Jan 21 16:47:32 2009 +0100
    28.3 @@ -16,21 +16,21 @@
    28.4  signature MORPHISM =
    28.5  sig
    28.6    include BASIC_MORPHISM
    28.7 -  val var: morphism -> Binding.T * mixfix -> Binding.T * mixfix
    28.8 -  val binding: morphism -> Binding.T -> Binding.T
    28.9 +  val var: morphism -> binding * mixfix -> binding * mixfix
   28.10 +  val binding: morphism -> binding -> binding
   28.11    val typ: morphism -> typ -> typ
   28.12    val term: morphism -> term -> term
   28.13    val fact: morphism -> thm list -> thm list
   28.14    val thm: morphism -> thm -> thm
   28.15    val cterm: morphism -> cterm -> cterm
   28.16    val morphism:
   28.17 -   {binding: Binding.T -> Binding.T,
   28.18 -    var: Binding.T * mixfix -> Binding.T * mixfix,
   28.19 +   {binding: binding -> binding,
   28.20 +    var: binding * mixfix -> binding * mixfix,
   28.21      typ: typ -> typ,
   28.22      term: term -> term,
   28.23      fact: thm list -> thm list} -> morphism
   28.24 -  val binding_morphism: (Binding.T -> Binding.T) -> morphism
   28.25 -  val var_morphism: (Binding.T * mixfix -> Binding.T * mixfix) -> morphism
   28.26 +  val binding_morphism: (binding -> binding) -> morphism
   28.27 +  val var_morphism: (binding * mixfix -> binding * mixfix) -> morphism
   28.28    val typ_morphism: (typ -> typ) -> morphism
   28.29    val term_morphism: (term -> term) -> morphism
   28.30    val fact_morphism: (thm list -> thm list) -> morphism
   28.31 @@ -45,8 +45,8 @@
   28.32  struct
   28.33  
   28.34  datatype morphism = Morphism of
   28.35 - {binding: Binding.T -> Binding.T,
   28.36 -  var: Binding.T * mixfix -> Binding.T * mixfix,
   28.37 + {binding: binding -> binding,
   28.38 +  var: binding * mixfix -> binding * mixfix,
   28.39    typ: typ -> typ,
   28.40    term: term -> term,
   28.41    fact: thm list -> thm list};
    29.1 --- a/src/Pure/sign.ML	Wed Jan 21 16:47:31 2009 +0100
    29.2 +++ b/src/Pure/sign.ML	Wed Jan 21 16:47:32 2009 +0100
    29.3 @@ -14,7 +14,7 @@
    29.4      tsig: Type.tsig,
    29.5      consts: Consts.T}
    29.6    val naming_of: theory -> NameSpace.naming
    29.7 -  val full_name: theory -> Binding.T -> string
    29.8 +  val full_name: theory -> binding -> string
    29.9    val base_name: string -> bstring
   29.10    val full_bname: theory -> bstring -> string
   29.11    val full_bname_path: theory -> string -> bstring -> string
   29.12 @@ -91,10 +91,10 @@
   29.13    val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
   29.14    val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
   29.15    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
   29.16 -  val declare_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
   29.17 +  val declare_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
   29.18    val add_consts: (bstring * string * mixfix) list -> theory -> theory
   29.19    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
   29.20 -  val add_abbrev: string -> Properties.T -> Binding.T * term -> theory -> (term * term) * theory
   29.21 +  val add_abbrev: string -> Properties.T -> binding * term -> theory -> (term * term) * theory
   29.22    val revert_abbrev: string -> string -> theory -> theory
   29.23    val add_const_constraint: string * typ option -> theory -> theory
   29.24    val primitive_class: string * class list -> theory -> theory
    30.1 --- a/src/Pure/theory.ML	Wed Jan 21 16:47:31 2009 +0100
    30.2 +++ b/src/Pure/theory.ML	Wed Jan 21 16:47:32 2009 +0100
    30.3 @@ -29,14 +29,14 @@
    30.4    val at_end: (theory -> theory option) -> theory -> theory
    30.5    val begin_theory: string -> theory list -> theory
    30.6    val end_theory: theory -> theory
    30.7 +  val add_axioms_i: (binding * term) list -> theory -> theory
    30.8    val add_axioms: (bstring * string) list -> theory -> theory
    30.9 -  val add_axioms_i: (bstring * term) list -> theory -> theory
   30.10    val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
   30.11 +  val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
   30.12    val add_defs: bool -> bool -> (bstring * string) list -> theory -> theory
   30.13 -  val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
   30.14 +  val add_finals_i: bool -> term list -> theory -> theory
   30.15    val add_finals: bool -> string list -> theory -> theory
   30.16 -  val add_finals_i: bool -> term list -> theory -> theory
   30.17 -  val specify_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
   30.18 +  val specify_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
   30.19  end
   30.20  
   30.21  structure Theory: THEORY =
   30.22 @@ -157,19 +157,19 @@
   30.23  fun err_in_axm msg name =
   30.24    cat_error msg ("The error(s) above occurred in axiom " ^ quote name);
   30.25  
   30.26 -fun cert_axm thy (name, raw_tm) =
   30.27 +fun cert_axm thy (b, raw_tm) =
   30.28    let
   30.29      val (t, T, _) = Sign.certify_prop thy raw_tm
   30.30        handle TYPE (msg, _, _) => error msg
   30.31          | TERM (msg, _) => error msg;
   30.32    in
   30.33      Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
   30.34 -    (name, Sign.no_vars (Syntax.pp_global thy) t)
   30.35 +    (b, Sign.no_vars (Syntax.pp_global thy) t)
   30.36    end;
   30.37  
   30.38 -fun read_axm thy (name, str) =
   30.39 -  cert_axm thy (name, Syntax.read_prop_global thy str)
   30.40 -    handle ERROR msg => err_in_axm msg name;
   30.41 +fun read_axm thy (bname, str) =
   30.42 +  cert_axm thy (Binding.name bname, Syntax.read_prop_global thy str)
   30.43 +    handle ERROR msg => err_in_axm msg bname;
   30.44  
   30.45  
   30.46  (* add_axioms(_i) *)
   30.47 @@ -178,15 +178,15 @@
   30.48  
   30.49  fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
   30.50    let
   30.51 -    val axms = map (apfst Binding.name o apsnd Logic.varify o prep_axm thy) raw_axms;
   30.52 +    val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
   30.53      val axioms' = fold (snd oo NameSpace.bind (Sign.naming_of thy)) axms axioms
   30.54        handle Symtab.DUP dup => err_dup_axm dup;
   30.55    in axioms' end);
   30.56  
   30.57  in
   30.58  
   30.59 +val add_axioms_i = gen_add_axioms cert_axm;
   30.60  val add_axioms = gen_add_axioms read_axm;
   30.61 -val add_axioms_i = gen_add_axioms cert_axm;
   30.62  
   30.63  end;
   30.64  
   30.65 @@ -250,16 +250,16 @@
   30.66  
   30.67  (* check_def *)
   30.68  
   30.69 -fun check_def thy unchecked overloaded (bname, tm) defs =
   30.70 +fun check_def thy unchecked overloaded (b, tm) defs =
   30.71    let
   30.72      val ctxt = ProofContext.init thy;
   30.73 -    val name = Sign.full_bname thy bname;
   30.74 +    val name = Sign.full_name thy b;
   30.75      val (lhs_const, rhs) = Sign.cert_def ctxt tm;
   30.76      val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
   30.77      val _ = check_overloading thy overloaded lhs_const;
   30.78    in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
   30.79    handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
   30.80 -   [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
   30.81 +   [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.display b) ^ ":"),
   30.82      Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
   30.83  
   30.84  
   30.85 @@ -298,8 +298,8 @@
   30.86  
   30.87  in
   30.88  
   30.89 +val add_finals_i = gen_add_finals (K I);
   30.90  val add_finals = gen_add_finals Syntax.read_term_global;
   30.91 -val add_finals_i = gen_add_finals (K I);
   30.92  
   30.93  end;
   30.94  
    31.1 --- a/src/Tools/induct.ML	Wed Jan 21 16:47:31 2009 +0100
    31.2 +++ b/src/Tools/induct.ML	Wed Jan 21 16:47:32 2009 +0100
    31.3 @@ -50,7 +50,7 @@
    31.4    val setN: string
    31.5    (*proof methods*)
    31.6    val fix_tac: Proof.context -> int -> (string * typ) list -> int -> tactic
    31.7 -  val add_defs: (Binding.T option * term) option list -> Proof.context ->
    31.8 +  val add_defs: (binding option * term) option list -> Proof.context ->
    31.9      (term option list * thm list) * Proof.context
   31.10    val atomize_term: theory -> term -> term
   31.11    val atomize_tac: int -> tactic
   31.12 @@ -62,7 +62,7 @@
   31.13    val cases_tac: Proof.context -> term option list list -> thm option ->
   31.14      thm list -> int -> cases_tactic
   31.15    val get_inductT: Proof.context -> term option list list -> thm list list
   31.16 -  val induct_tac: Proof.context -> (Binding.T option * term) option list list ->
   31.17 +  val induct_tac: Proof.context -> (binding option * term) option list list ->
   31.18      (string * typ) list list -> term option list -> thm list option ->
   31.19      thm list -> int -> cases_tactic
   31.20    val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->