src/Pure/consts.ML
changeset 28861 f53abb0733ee
parent 28017 4919bd124a58
child 28965 1de908189869
     1.1 --- a/src/Pure/consts.ML	Thu Nov 20 14:51:40 2008 +0100
     1.2 +++ b/src/Pure/consts.ML	Thu Nov 20 14:55:25 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 -> (bstring * typ) -> T -> T
     1.8 +  val declare: bool -> NameSpace.naming -> Properties.T -> (Name.binding * 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 -    bstring * term -> T -> (term * term) * T
    1.12 +    Name.binding * 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.extend_table naming [decl] tab
    1.21 +fun extend_decls naming decl tab = NameSpace.table_declare naming decl tab
    1.22    handle Symtab.DUP c => err_dup_const c;
    1.23  
    1.24  
    1.25 @@ -223,11 +223,11 @@
    1.26  
    1.27  (* declarations *)
    1.28  
    1.29 -fun declare authentic naming tags (c, declT) = map_consts (fn (decls, constraints, rev_abbrevs) =>
    1.30 +fun declare authentic naming tags (b, declT) = map_consts (fn (decls, constraints, rev_abbrevs) =>
    1.31    let
    1.32      val tags' = tags |> Position.default_properties (Position.thread_data ());
    1.33      val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
    1.34 -    val decls' = decls |> extend_decls naming (c, ((decl, NONE), serial ()));
    1.35 +    val (_, decls') = decls |> extend_decls naming (b, ((decl, NONE), serial ()));
    1.36    in (decls', constraints, rev_abbrevs) end);
    1.37  
    1.38  
    1.39 @@ -262,7 +262,7 @@
    1.40  
    1.41  in
    1.42  
    1.43 -fun abbreviate pp tsig naming mode tags (c, raw_rhs) consts =
    1.44 +fun abbreviate pp tsig naming mode tags (b, raw_rhs) consts =
    1.45    let
    1.46      val cert_term = certify pp tsig false consts;
    1.47      val expand_term = certify pp tsig true consts;
    1.48 @@ -273,7 +273,7 @@
    1.49        |> cert_term;
    1.50      val normal_rhs = expand_term rhs;
    1.51      val T = Term.fastype_of rhs;
    1.52 -    val lhs = Const (NameSpace.full naming c, T);
    1.53 +    val lhs = Const (NameSpace.full_binding naming b, T);
    1.54  
    1.55      fun err msg = error (msg ^ " on rhs of abbreviation:\n" ^
    1.56        Pretty.string_of_term pp (Logic.mk_equals (lhs, rhs)));
    1.57 @@ -285,8 +285,8 @@
    1.58          val tags' = tags |> Position.default_properties (Position.thread_data ());
    1.59          val decl = {T = T, typargs = typargs_of T, tags = tags', authentic = true};
    1.60          val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
    1.61 -        val decls' = decls
    1.62 -          |> extend_decls naming (c, ((decl, SOME abbr), serial ()));
    1.63 +        val (_, decls') = decls
    1.64 +          |> extend_decls naming (b, ((decl, SOME abbr), serial ()));
    1.65          val rev_abbrevs' = rev_abbrevs
    1.66            |> fold (curry Symtab.cons_list mode) (rev_abbrev lhs rhs);
    1.67        in (decls', constraints, rev_abbrevs') end)