src/Pure/sign.ML
changeset 28017 4919bd124a58
parent 27302 8d12ac6a3e1c
child 28111 ea22fd4685fb
     1.1 --- a/src/Pure/sign.ML	Wed Aug 27 11:24:35 2008 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed Aug 27 11:48:54 2008 +0200
     1.3 @@ -93,9 +93,8 @@
     1.4    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
     1.5    val add_consts: (bstring * string * mixfix) list -> theory -> theory
     1.6    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
     1.7 -  val declare_const: Markup.property list -> bstring * typ * mixfix -> theory -> term * theory
     1.8 -  val add_abbrev: string -> Markup.property list ->
     1.9 -    bstring * term -> theory -> (term * term) * theory
    1.10 +  val declare_const: Properties.T -> bstring * typ * mixfix -> theory -> term * theory
    1.11 +  val add_abbrev: string -> Properties.T -> bstring * term -> theory -> (term * term) * theory
    1.12    val revert_abbrev: string -> string -> theory -> theory
    1.13    val add_const_constraint: string * typ option -> theory -> theory
    1.14    val primitive_class: string * class list -> theory -> theory
    1.15 @@ -515,7 +514,7 @@
    1.16          val T' = Logic.varifyT T;
    1.17        in ((c, T'), (c', T', mx), Const (full_c, T)) end;
    1.18      val args = map prep raw_args;
    1.19 -    val tags' = tags |> AList.update (op =) (Markup.theory_nameN, Context.theory_name thy);
    1.20 +    val tags' = tags |> Properties.put (Markup.theory_nameN, Context.theory_name thy);
    1.21    in
    1.22      thy
    1.23      |> map_consts (fold (Consts.declare authentic (naming_of thy) tags' o #1) args)