src/Pure/consts.ML
changeset 28965 1de908189869
parent 28861 f53abb0733ee
child 29251 8f84a608883d
     1.1 --- a/src/Pure/consts.ML	Wed Dec 03 21:00:39 2008 -0800
     1.2 +++ b/src/Pure/consts.ML	Thu Dec 04 14:43:33 2008 +0100
     1.3 @@ -30,10 +30,10 @@
     1.4    val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
     1.5    val typargs: T -> string * typ -> typ list
     1.6    val instance: T -> string * typ list -> typ
     1.7 -  val declare: bool -> NameSpace.naming -> Properties.T -> (Name.binding * typ) -> T -> T
     1.8 +  val declare: bool -> NameSpace.naming -> Properties.T -> (Binding.T * typ) -> T -> T
     1.9    val constrain: string * typ option -> T -> T
    1.10    val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
    1.11 -    Name.binding * term -> T -> (term * term) * T
    1.12 +    Binding.T * term -> T -> (term * term) * T
    1.13    val revert_abbrev: string -> string -> T -> T
    1.14    val hide: bool -> string -> T -> T
    1.15    val empty: T
    1.16 @@ -211,7 +211,7 @@
    1.17  fun err_dup_const c =
    1.18    error ("Duplicate declaration of constant " ^ quote c);
    1.19  
    1.20 -fun extend_decls naming decl tab = NameSpace.table_declare naming decl tab
    1.21 +fun extend_decls naming decl tab = NameSpace.bind naming decl tab
    1.22    handle Symtab.DUP c => err_dup_const c;
    1.23  
    1.24  
    1.25 @@ -273,7 +273,7 @@
    1.26        |> cert_term;
    1.27      val normal_rhs = expand_term rhs;
    1.28      val T = Term.fastype_of rhs;
    1.29 -    val lhs = Const (NameSpace.full_binding naming b, T);
    1.30 +    val lhs = Const (NameSpace.full_name naming b, T);
    1.31  
    1.32      fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^
    1.33        Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs)));