src/Pure/consts.ML
changeset 28017 4919bd124a58
parent 26050 88bb26089ef5
child 28861 f53abb0733ee
     1.1 --- a/src/Pure/consts.ML	Wed Aug 27 11:24:35 2008 +0200
     1.2 +++ b/src/Pure/consts.ML	Wed Aug 27 11:48:54 2008 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    val the_type: T -> string -> typ                             (*exception TYPE*)
     1.5    val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
     1.6    val type_scheme: T -> string -> typ                          (*exception TYPE*)
     1.7 -  val the_tags: T -> string -> Markup.property list            (*exception TYPE*)
     1.8 +  val the_tags: T -> string -> Properties.T                    (*exception TYPE*)
     1.9    val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
    1.10    val the_constraint: T -> string -> typ                       (*exception TYPE*)
    1.11    val space_of: T -> NameSpace.T
    1.12 @@ -30,9 +30,9 @@
    1.13    val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
    1.14    val typargs: T -> string * typ -> typ list
    1.15    val instance: T -> string * typ list -> typ
    1.16 -  val declare: bool -> NameSpace.naming -> Markup.property list -> (bstring * typ) -> T -> T
    1.17 +  val declare: bool -> NameSpace.naming -> Properties.T -> (bstring * typ) -> T -> T
    1.18    val constrain: string * typ option -> T -> T
    1.19 -  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Markup.property list ->
    1.20 +  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
    1.21      bstring * term -> T -> (term * term) * T
    1.22    val revert_abbrev: string -> string -> T -> T
    1.23    val hide: bool -> string -> T -> T
    1.24 @@ -47,7 +47,7 @@
    1.25  
    1.26  (* datatype T *)
    1.27  
    1.28 -type decl = {T: typ, typargs: int list list, tags: Markup.property list, authentic: bool};
    1.29 +type decl = {T: typ, typargs: int list list, tags: Properties.T, authentic: bool};
    1.30  type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
    1.31  
    1.32  datatype T = Consts of