src/Pure/sign.ML
changeset 29581 b3b33e0298eb
parent 29006 abe0f11cfa4e
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/sign.ML	Wed Jan 21 16:47:31 2009 +0100
     1.2 +++ b/src/Pure/sign.ML	Wed Jan 21 16:47:32 2009 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4      tsig: Type.tsig,
     1.5      consts: Consts.T}
     1.6    val naming_of: theory -> NameSpace.naming
     1.7 -  val full_name: theory -> Binding.T -> string
     1.8 +  val full_name: theory -> binding -> string
     1.9    val base_name: string -> bstring
    1.10    val full_bname: theory -> bstring -> string
    1.11    val full_bname_path: theory -> string -> bstring -> string
    1.12 @@ -91,10 +91,10 @@
    1.13    val del_modesyntax: Syntax.mode -> (bstring * string * mixfix) list -> theory -> theory
    1.14    val del_modesyntax_i: Syntax.mode -> (bstring * typ * mixfix) list -> theory -> theory
    1.15    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
    1.16 -  val declare_const: Properties.T -> (Binding.T * typ) * mixfix -> theory -> term * theory
    1.17 +  val declare_const: Properties.T -> (binding * typ) * mixfix -> theory -> term * theory
    1.18    val add_consts: (bstring * string * mixfix) list -> theory -> theory
    1.19    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    1.20 -  val add_abbrev: string -> Properties.T -> Binding.T * term -> theory -> (term * term) * theory
    1.21 +  val add_abbrev: string -> Properties.T -> binding * term -> theory -> (term * term) * theory
    1.22    val revert_abbrev: string -> string -> theory -> theory
    1.23    val add_const_constraint: string * typ option -> theory -> theory
    1.24    val primitive_class: string * class list -> theory -> theory