type Properties.T;
authorwenzelm
Wed Aug 27 11:48:54 2008 +0200 (2008-08-27)
changeset 280174919bd124a58
parent 28016 b46f48256dab
child 28018 d3c5ab88fdcd
type Properties.T;
doc-src/IsarImplementation/Thy/ML.thy
doc-src/IsarImplementation/Thy/logic.thy
src/Pure/General/markup.ML
src/Pure/General/position.ML
src/Pure/General/xml.ML
src/Pure/Isar/class.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/proof_context.ML
src/Pure/ProofGeneral/pgip_types.ML
src/Pure/Tools/xml_syntax.ML
src/Pure/consts.ML
src/Pure/more_thm.ML
src/Pure/sign.ML
src/Pure/theory.ML
src/Pure/thm.ML
src/Pure/type.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Wed Aug 27 11:24:35 2008 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Wed Aug 27 11:48:54 2008 +0200
     1.3 @@ -317,7 +317,7 @@
     1.4    a theory by constant declararion and primitive definitions:
     1.5  
     1.6    \smallskip\begin{mldecls}
     1.7 -  @{ML "Sign.declare_const: Markup.property list -> bstring * typ * mixfix
     1.8 +  @{ML "Sign.declare_const: Properties.T -> bstring * typ * mixfix
     1.9    -> theory -> term * theory"} \\
    1.10    @{ML "Thm.add_def: bool -> bool -> bstring * term -> theory -> thm * theory"}
    1.11    \end{mldecls}
     2.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Wed Aug 27 11:24:35 2008 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Wed Aug 27 11:48:54 2008 +0200
     2.3 @@ -326,9 +326,9 @@
     2.4    @{index_ML fastype_of: "term -> typ"} \\
     2.5    @{index_ML lambda: "term -> term -> term"} \\
     2.6    @{index_ML betapply: "term * term -> term"} \\
     2.7 -  @{index_ML Sign.declare_const: "Markup.property list -> bstring * typ * mixfix ->
     2.8 +  @{index_ML Sign.declare_const: "Properties.T -> bstring * typ * mixfix ->
     2.9    theory -> term * theory"} \\
    2.10 -  @{index_ML Sign.add_abbrev: "string -> Markup.property list -> bstring * term ->
    2.11 +  @{index_ML Sign.add_abbrev: "string -> Properties.T -> bstring * term ->
    2.12    theory -> (term * term) * theory"} \\
    2.13    @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
    2.14    @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
     3.1 --- a/src/Pure/General/markup.ML	Wed Aug 27 11:24:35 2008 +0200
     3.2 +++ b/src/Pure/General/markup.ML	Wed Aug 27 11:48:54 2008 +0200
     3.3 @@ -7,8 +7,7 @@
     3.4  
     3.5  signature MARKUP =
     3.6  sig
     3.7 -  type property = string * string
     3.8 -  type T = string * property list
     3.9 +  type T = string * Properties.T
    3.10    val get_string: T -> string -> string option
    3.11    val get_int: T -> string -> int option
    3.12    val none: T
    3.13 @@ -21,7 +20,7 @@
    3.14    val idN: string
    3.15    val kindN: string
    3.16    val internalK: string
    3.17 -  val property_internal: property
    3.18 +  val property_internal: Properties.property
    3.19    val lineN: string
    3.20    val columnN: string
    3.21    val offsetN: string
    3.22 @@ -116,8 +115,7 @@
    3.23  
    3.24  (* basic markup *)
    3.25  
    3.26 -type property = string * string;
    3.27 -type T = string * property list;
    3.28 +type T = string * Properties.T;
    3.29  
    3.30  val none = ("", []);
    3.31  
    3.32 @@ -126,9 +124,9 @@
    3.33  
    3.34  
    3.35  fun properties more_props ((elem, props): T) =
    3.36 -  (elem, fold_rev (AList.update (op =)) more_props props);
    3.37 +  (elem, fold_rev Properties.put more_props props);
    3.38  
    3.39 -fun get_string ((_, props): T) prop = AList.lookup (op =) props prop;
    3.40 +fun get_string (_, props) = Properties.get props;
    3.41  fun get_int m prop = (case get_string m prop of NONE => NONE | SOME s => Int.fromString s);
    3.42  
    3.43  fun markup_elem elem = (elem, (elem, []): T);
     4.1 --- a/src/Pure/General/position.ML	Wed Aug 27 11:24:35 2008 +0200
     4.2 +++ b/src/Pure/General/position.ML	Wed Aug 27 11:48:54 2008 +0200
     4.3 @@ -21,9 +21,9 @@
     4.4    val line_file: int -> string -> T
     4.5    val get_id: T -> string option
     4.6    val put_id: string -> T -> T
     4.7 -  val of_properties: Markup.property list -> T
     4.8 -  val properties_of: T -> Markup.property list
     4.9 -  val default_properties: T -> Markup.property list -> Markup.property list
    4.10 +  val of_properties: Properties.T -> T
    4.11 +  val properties_of: T -> Properties.T
    4.12 +  val default_properties: T -> Properties.T -> Properties.T
    4.13    val report: Markup.T -> T -> unit
    4.14    val str_of: T -> string
    4.15    type range = T * T
    4.16 @@ -41,7 +41,7 @@
    4.17  
    4.18  (* datatype position *)
    4.19  
    4.20 -datatype T = Pos of (int * int * int) * Markup.property list;
    4.21 +datatype T = Pos of (int * int * int) * Properties.T;
    4.22  
    4.23  fun valid (i: int) = i > 0;
    4.24  fun if_valid i i' = if valid i then i' else i;
    4.25 @@ -55,7 +55,7 @@
    4.26  fun column_of (Pos ((_, j, _), _)) = if valid j then SOME j else NONE;
    4.27  fun offset_of (Pos ((_, _, k), _)) = if valid k then SOME k else NONE;
    4.28  
    4.29 -fun file_of (Pos (_, props)) = AList.lookup (op =) props Markup.fileN;
    4.30 +fun file_of (Pos (_, props)) = Properties.get props Markup.fileN;
    4.31  
    4.32  
    4.33  (* advance *)
    4.34 @@ -97,13 +97,13 @@
    4.35  
    4.36  (* markup properties *)
    4.37  
    4.38 -fun get_id (Pos (_, props)) = AList.lookup (op =) props Markup.idN;
    4.39 -fun put_id id (Pos (count, props)) = Pos (count, AList.update (op =) (Markup.idN, id) props);
    4.40 +fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
    4.41 +fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
    4.42  
    4.43  fun of_properties props =
    4.44    let
    4.45      fun get name =
    4.46 -      (case AList.lookup (op =) props name of
    4.47 +      (case Properties.get props name of
    4.48          NONE => 0
    4.49        | SOME s => the_default 0 (Int.fromString s));
    4.50      val count = (get Markup.lineN, get Markup.columnN, get Markup.offsetN);
    4.51 @@ -145,12 +145,12 @@
    4.52  val no_range = (none, none);
    4.53  
    4.54  fun encode_range (Pos (count, props), Pos ((i, j, k), _)) =
    4.55 -  let val props' = props |> fold_rev (AList.update op =)
    4.56 +  let val props' = props |> fold_rev Properties.put
    4.57      (value Markup.end_lineN i @ value Markup.end_columnN j @ value Markup.end_offsetN k)
    4.58    in Pos (count, props') end;
    4.59  
    4.60  fun reset_range (Pos (count, props)) =
    4.61 -  let val props' = props |> fold (AList.delete op =)
    4.62 +  let val props' = props |> fold Properties.remove
    4.63      [Markup.end_lineN, Markup.end_columnN, Markup.end_offsetN]
    4.64    in Pos (count, props') end;
    4.65  
     5.1 --- a/src/Pure/General/xml.ML	Wed Aug 27 11:24:35 2008 +0200
     5.2 +++ b/src/Pure/General/xml.ML	Wed Aug 27 11:48:54 2008 +0200
     5.3 @@ -7,7 +7,7 @@
     5.4  
     5.5  signature XML =
     5.6  sig
     5.7 -  type attributes = Markup.property list
     5.8 +  type attributes = Properties.T
     5.9    datatype tree =
    5.10        Elem of string * attributes * tree list
    5.11      | Text of string
    5.12 @@ -32,7 +32,7 @@
    5.13  
    5.14  (** XML trees **)
    5.15  
    5.16 -type attributes = Markup.property list;
    5.17 +type attributes = Properties.T;
    5.18  
    5.19  datatype tree =
    5.20      Elem of string * attributes * tree list
     6.1 --- a/src/Pure/Isar/class.ML	Wed Aug 27 11:24:35 2008 +0200
     6.2 +++ b/src/Pure/Isar/class.ML	Wed Aug 27 11:48:54 2008 +0200
     6.3 @@ -14,9 +14,9 @@
     6.4      -> theory -> string * Proof.context
     6.5  
     6.6    val init: class -> theory -> Proof.context
     6.7 -  val declare: class -> Markup.property list
     6.8 +  val declare: class -> Properties.T
     6.9      -> (string * mixfix) * term -> theory -> theory
    6.10 -  val abbrev: class -> Syntax.mode -> Markup.property list
    6.11 +  val abbrev: class -> Syntax.mode -> Properties.T
    6.12      -> (string * mixfix) * term -> theory -> theory
    6.13    val note: class -> string
    6.14      -> ((string * Attrib.src list) * (thm list * Attrib.src list) list) list
     7.1 --- a/src/Pure/Isar/local_theory.ML	Wed Aug 27 11:24:35 2008 +0200
     7.2 +++ b/src/Pure/Isar/local_theory.ML	Wed Aug 27 11:48:54 2008 +0200
     7.3 @@ -11,8 +11,8 @@
     7.4  sig
     7.5    type operations
     7.6    val group_of: local_theory -> string
     7.7 -  val group_properties_of: local_theory -> Markup.property list
     7.8 -  val group_position_of: local_theory -> Markup.property list
     7.9 +  val group_properties_of: local_theory -> Properties.T
    7.10 +  val group_position_of: local_theory -> Properties.T
    7.11    val set_group: string -> local_theory -> local_theory
    7.12    val target_of: local_theory -> Proof.context
    7.13    val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
     8.1 --- a/src/Pure/Isar/outer_parse.ML	Wed Aug 27 11:24:35 2008 +0200
     8.2 +++ b/src/Pure/Isar/outer_parse.ML	Wed Aug 27 11:48:54 2008 +0200
     8.3 @@ -60,7 +60,7 @@
     8.4      'a * token list -> 'b list * ('a * token list)
     8.5    val list: (token list -> 'a * token list) -> token list -> 'a list * token list
     8.6    val list1: (token list -> 'a * token list) -> token list -> 'a list * token list
     8.7 -  val properties: token list -> Markup.property list * token list
     8.8 +  val properties: token list -> Properties.T * token list
     8.9    val name: token list -> bstring * token list
    8.10    val xname: token list -> xstring * token list
    8.11    val text: token list -> string * token list
     9.1 --- a/src/Pure/Isar/proof_context.ML	Wed Aug 27 11:24:35 2008 +0200
     9.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Aug 27 11:48:54 2008 +0200
     9.3 @@ -131,7 +131,7 @@
     9.4    val target_notation: bool -> Syntax.mode -> (term * mixfix) list -> morphism ->
     9.5      Context.generic -> Context.generic
     9.6    val add_const_constraint: string * typ option -> Proof.context -> Proof.context
     9.7 -  val add_abbrev: string -> Markup.property list ->
     9.8 +  val add_abbrev: string -> Properties.T ->
     9.9      bstring * term -> Proof.context -> (term * term) * Proof.context
    9.10    val revert_abbrev: string -> string -> Proof.context -> Proof.context
    9.11    val verbose: bool ref
    9.12 @@ -145,9 +145,9 @@
    9.13    val prems_limit: int ref
    9.14    val pretty_ctxt: Proof.context -> Pretty.T list
    9.15    val pretty_context: Proof.context -> Pretty.T list
    9.16 -  val query_type: Proof.context -> string -> Markup.property list
    9.17 -  val query_const: Proof.context -> string -> Markup.property list
    9.18 -  val query_class: Proof.context -> string -> Markup.property list
    9.19 +  val query_type: Proof.context -> string -> Properties.T
    9.20 +  val query_const: Proof.context -> string -> Properties.T
    9.21 +  val query_class: Proof.context -> string -> Properties.T
    9.22  end;
    9.23  
    9.24  structure ProofContext: PROOF_CONTEXT =
    10.1 --- a/src/Pure/ProofGeneral/pgip_types.ML	Wed Aug 27 11:24:35 2008 +0200
    10.2 +++ b/src/Pure/ProofGeneral/pgip_types.ML	Wed Aug 27 11:48:54 2008 +0200
    10.3 @@ -112,9 +112,9 @@
    10.4  
    10.5  (** XML utils **)
    10.6  
    10.7 -fun has_attr (attr : string) attrs = AList.defined (op =) attrs attr
    10.8 +fun has_attr attr attrs = Properties.defined attrs attr
    10.9  
   10.10 -fun get_attr_opt (attr : string) attrs = AList.lookup (op =) attrs attr
   10.11 +fun get_attr_opt attr attrs = Properties.get attrs attr
   10.12  
   10.13  fun get_attr attr attrs =
   10.14      (case get_attr_opt attr attrs of
    11.1 --- a/src/Pure/Tools/xml_syntax.ML	Wed Aug 27 11:24:35 2008 +0200
    11.2 +++ b/src/Pure/Tools/xml_syntax.ML	Wed Aug 27 11:48:54 2008 +0200
    11.3 @@ -102,11 +102,11 @@
    11.4    NONE => raise XML (s ^ ": bad index", tree) | SOME i => i);
    11.5  
    11.6  fun type_of_xml (tree as XML.Elem ("TVar", atts, classes)) = TVar
    11.7 -      ((case AList.lookup op = atts "name" of
    11.8 +      ((case Properties.get atts "name" of
    11.9            NONE => raise XML ("type_of_xml: name of TVar missing", tree)
   11.10          | SOME name => name,
   11.11          the_default 0 (Option.map (index_of_string "type_of_xml" tree)
   11.12 -          (AList.lookup op = atts "index"))),
   11.13 +          (Properties.get atts "index"))),
   11.14         map class_of_xml classes)
   11.15    | type_of_xml (XML.Elem ("TFree", [("name", s)], classes)) =
   11.16        TFree (s, map class_of_xml classes)
   11.17 @@ -119,11 +119,11 @@
   11.18    | term_of_xml (XML.Elem ("Free", [("name", s)], [typ])) =
   11.19        Free (s, type_of_xml typ)
   11.20    | term_of_xml (tree as XML.Elem ("Var", atts, [typ])) = Var
   11.21 -      ((case AList.lookup op = atts "name" of
   11.22 +      ((case Properties.get atts "name" of
   11.23            NONE => raise XML ("type_of_xml: name of Var missing", tree)
   11.24          | SOME name => name,
   11.25          the_default 0 (Option.map (index_of_string "term_of_xml" tree)
   11.26 -          (AList.lookup op = atts "index"))),
   11.27 +          (Properties.get atts "index"))),
   11.28         type_of_xml typ)
   11.29    | term_of_xml (XML.Elem ("Const", [("name", s)], [typ])) =
   11.30        Const (s, type_of_xml typ)
    12.1 --- a/src/Pure/consts.ML	Wed Aug 27 11:24:35 2008 +0200
    12.2 +++ b/src/Pure/consts.ML	Wed Aug 27 11:48:54 2008 +0200
    12.3 @@ -17,7 +17,7 @@
    12.4    val the_type: T -> string -> typ                             (*exception TYPE*)
    12.5    val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
    12.6    val type_scheme: T -> string -> typ                          (*exception TYPE*)
    12.7 -  val the_tags: T -> string -> Markup.property list            (*exception TYPE*)
    12.8 +  val the_tags: T -> string -> Properties.T                    (*exception TYPE*)
    12.9    val is_monomorphic: T -> string -> bool                      (*exception TYPE*)
   12.10    val the_constraint: T -> string -> typ                       (*exception TYPE*)
   12.11    val space_of: T -> NameSpace.T
   12.12 @@ -30,9 +30,9 @@
   12.13    val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   12.14    val typargs: T -> string * typ -> typ list
   12.15    val instance: T -> string * typ list -> typ
   12.16 -  val declare: bool -> NameSpace.naming -> Markup.property list -> (bstring * typ) -> T -> T
   12.17 +  val declare: bool -> NameSpace.naming -> Properties.T -> (bstring * typ) -> T -> T
   12.18    val constrain: string * typ option -> T -> T
   12.19 -  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Markup.property list ->
   12.20 +  val abbreviate: Pretty.pp -> Type.tsig -> NameSpace.naming -> string -> Properties.T ->
   12.21      bstring * term -> T -> (term * term) * T
   12.22    val revert_abbrev: string -> string -> T -> T
   12.23    val hide: bool -> string -> T -> T
   12.24 @@ -47,7 +47,7 @@
   12.25  
   12.26  (* datatype T *)
   12.27  
   12.28 -type decl = {T: typ, typargs: int list list, tags: Markup.property list, authentic: bool};
   12.29 +type decl = {T: typ, typargs: int list list, tags: Properties.T, authentic: bool};
   12.30  type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
   12.31  
   12.32  datatype T = Consts of
    13.1 --- a/src/Pure/more_thm.ML	Wed Aug 27 11:24:35 2008 +0200
    13.2 +++ b/src/Pure/more_thm.ML	Wed Aug 27 11:48:54 2008 +0200
    13.3 @@ -46,9 +46,9 @@
    13.4    val proof_attributes: attribute list -> Proof.context * thm -> Proof.context * thm
    13.5    val no_attributes: 'a -> 'a * 'b list
    13.6    val simple_fact: 'a -> ('a * 'b list) list
    13.7 -  val tag_rule: Markup.property -> thm -> thm
    13.8 +  val tag_rule: Properties.property -> thm -> thm
    13.9    val untag_rule: string -> thm -> thm
   13.10 -  val tag: Markup.property -> attribute
   13.11 +  val tag: Properties.property -> attribute
   13.12    val untag: string -> attribute
   13.13    val position_of: thm -> Position.T
   13.14    val default_position: Position.T -> thm -> thm
   13.15 @@ -71,7 +71,7 @@
   13.16    val kind_rule: string -> thm -> thm
   13.17    val kind: string -> attribute
   13.18    val kind_internal: attribute
   13.19 -  val has_internal: Markup.property list -> bool
   13.20 +  val has_internal: Properties.property list -> bool
   13.21    val is_internal: thm -> bool
   13.22  end;
   13.23  
   13.24 @@ -337,10 +337,9 @@
   13.25  
   13.26  (* theorem groups *)
   13.27  
   13.28 -fun get_group thm = AList.lookup (op =) (Thm.get_tags thm) Markup.groupN;
   13.29 +fun get_group thm = Properties.get (Thm.get_tags thm) Markup.groupN;
   13.30  
   13.31 -fun put_group name =
   13.32 -  if name = "" then I else Thm.map_tags (AList.update (op =) (Markup.groupN, name));
   13.33 +fun put_group name = if name = "" then I else Thm.map_tags (Properties.put (Markup.groupN, name));
   13.34  
   13.35  fun group name = rule_attribute (K (put_group name));
   13.36  
   13.37 @@ -355,7 +354,7 @@
   13.38  val corollaryK = "corollary";
   13.39  val internalK = Markup.internalK;
   13.40  
   13.41 -fun the_kind thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.kindN);
   13.42 +fun the_kind thm = the (Properties.get (Thm.get_tags thm) Markup.kindN);
   13.43  
   13.44  val has_kind = can the_kind;
   13.45  val get_kind = the_default "" o try the_kind;
    14.1 --- a/src/Pure/sign.ML	Wed Aug 27 11:24:35 2008 +0200
    14.2 +++ b/src/Pure/sign.ML	Wed Aug 27 11:48:54 2008 +0200
    14.3 @@ -93,9 +93,8 @@
    14.4    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
    14.5    val add_consts: (bstring * string * mixfix) list -> theory -> theory
    14.6    val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory
    14.7 -  val declare_const: Markup.property list -> bstring * typ * mixfix -> theory -> term * theory
    14.8 -  val add_abbrev: string -> Markup.property list ->
    14.9 -    bstring * term -> theory -> (term * term) * theory
   14.10 +  val declare_const: Properties.T -> bstring * typ * mixfix -> theory -> term * theory
   14.11 +  val add_abbrev: string -> Properties.T -> bstring * term -> theory -> (term * term) * theory
   14.12    val revert_abbrev: string -> string -> theory -> theory
   14.13    val add_const_constraint: string * typ option -> theory -> theory
   14.14    val primitive_class: string * class list -> theory -> theory
   14.15 @@ -515,7 +514,7 @@
   14.16          val T' = Logic.varifyT T;
   14.17        in ((c, T'), (c', T', mx), Const (full_c, T)) end;
   14.18      val args = map prep raw_args;
   14.19 -    val tags' = tags |> AList.update (op =) (Markup.theory_nameN, Context.theory_name thy);
   14.20 +    val tags' = tags |> Properties.put (Markup.theory_nameN, Context.theory_name thy);
   14.21    in
   14.22      thy
   14.23      |> map_consts (fold (Consts.declare authentic (naming_of thy) tags' o #1) args)
    15.1 --- a/src/Pure/theory.ML	Wed Aug 27 11:24:35 2008 +0200
    15.2 +++ b/src/Pure/theory.ML	Wed Aug 27 11:48:54 2008 +0200
    15.3 @@ -38,7 +38,7 @@
    15.4    val add_defs_i: bool -> bool -> (bstring * term) list -> theory -> theory
    15.5    val add_finals: bool -> string list -> theory -> theory
    15.6    val add_finals_i: bool -> term list -> theory -> theory
    15.7 -  val specify_const: Markup.property list -> bstring * typ * mixfix -> (string * typ) list ->
    15.8 +  val specify_const: Properties.T -> bstring * typ * mixfix -> (string * typ) list ->
    15.9     theory -> term * theory
   15.10    val add_oracle: bstring * (theory * Object.T -> term) -> theory -> theory
   15.11  end
    16.1 --- a/src/Pure/thm.ML	Wed Aug 27 11:24:35 2008 +0200
    16.2 +++ b/src/Pure/thm.ML	Wed Aug 27 11:48:54 2008 +0200
    16.3 @@ -42,7 +42,7 @@
    16.4    val rep_thm: thm ->
    16.5     {thy_ref: theory_ref,
    16.6      der: bool * Proofterm.proof,
    16.7 -    tags: Markup.property list,
    16.8 +    tags: Properties.T,
    16.9      maxidx: int,
   16.10      shyps: sort list,
   16.11      hyps: term list,
   16.12 @@ -51,7 +51,7 @@
   16.13    val crep_thm: thm ->
   16.14     {thy_ref: theory_ref,
   16.15      der: bool * Proofterm.proof,
   16.16 -    tags: Markup.property list,
   16.17 +    tags: Properties.T,
   16.18      maxidx: int,
   16.19      shyps: sort list,
   16.20      hyps: cterm list,
   16.21 @@ -138,8 +138,8 @@
   16.22    val full_prop_of: thm -> term
   16.23    val get_name: thm -> string
   16.24    val put_name: string -> thm -> thm
   16.25 -  val get_tags: thm -> Markup.property list
   16.26 -  val map_tags: (Markup.property list -> Markup.property list) -> thm -> thm
   16.27 +  val get_tags: thm -> Properties.T
   16.28 +  val map_tags: (Properties.T -> Properties.T) -> thm -> thm
   16.29    val norm_proof: thm -> thm
   16.30    val adjust_maxidx_thm: int -> thm -> thm
   16.31    val rename_boundvars: term -> term -> thm -> thm
   16.32 @@ -338,7 +338,7 @@
   16.33  abstype thm = Thm of
   16.34   {thy_ref: theory_ref,         (*dynamic reference to theory*)
   16.35    der: bool * Pt.proof,        (*derivation*)
   16.36 -  tags: Markup.property list,  (*additional annotations/comments*)
   16.37 +  tags: Properties.T,          (*additional annotations/comments*)
   16.38    maxidx: int,                 (*maximum index of any Var or TVar*)
   16.39    shyps: sort list,            (*sort hypotheses as ordered list*)
   16.40    hyps: term list,             (*hypotheses as ordered list*)
    17.1 --- a/src/Pure/type.ML	Wed Aug 27 11:24:35 2008 +0200
    17.2 +++ b/src/Pure/type.ML	Wed Aug 27 11:48:54 2008 +0200
    17.3 @@ -17,7 +17,7 @@
    17.4    val rep_tsig: tsig ->
    17.5     {classes: NameSpace.T * Sorts.algebra,
    17.6      default: sort,
    17.7 -    types: ((decl * Markup.property list) * serial) NameSpace.table,
    17.8 +    types: ((decl * Properties.T) * serial) NameSpace.table,
    17.9      log_types: string list}
   17.10    val empty_tsig: tsig
   17.11    val defaultS: tsig -> sort
   17.12 @@ -40,7 +40,7 @@
   17.13    val cert_typ: tsig -> typ -> typ
   17.14    val arity_number: tsig -> string -> int
   17.15    val arity_sorts: Pretty.pp -> tsig -> string -> sort -> sort list
   17.16 -  val the_tags: tsig -> string -> Markup.property list
   17.17 +  val the_tags: tsig -> string -> Properties.T
   17.18  
   17.19    (*special treatment of type vars*)
   17.20    val strip_sorts: typ -> typ
   17.21 @@ -73,9 +73,9 @@
   17.22    val add_class: Pretty.pp -> NameSpace.naming -> bstring * class list -> tsig -> tsig
   17.23    val hide_class: bool -> string -> tsig -> tsig
   17.24    val set_defsort: sort -> tsig -> tsig
   17.25 -  val add_type: NameSpace.naming -> Markup.property list -> bstring * int -> tsig -> tsig
   17.26 -  val add_abbrev: NameSpace.naming -> Markup.property list -> string * string list * typ -> tsig -> tsig
   17.27 -  val add_nonterminal: NameSpace.naming -> Markup.property list -> string -> tsig -> tsig
   17.28 +  val add_type: NameSpace.naming -> Properties.T -> bstring * int -> tsig -> tsig
   17.29 +  val add_abbrev: NameSpace.naming -> Properties.T -> string * string list * typ -> tsig -> tsig
   17.30 +  val add_nonterminal: NameSpace.naming -> Properties.T -> string -> tsig -> tsig
   17.31    val hide_type: bool -> string -> tsig -> tsig
   17.32    val add_arity: Pretty.pp -> arity -> tsig -> tsig
   17.33    val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
   17.34 @@ -105,7 +105,7 @@
   17.35    TSig of {
   17.36      classes: NameSpace.T * Sorts.algebra,   (*order-sorted algebra of type classes*)
   17.37      default: sort,                          (*default sort on input*)
   17.38 -    types: ((decl * Markup.property list) * serial) NameSpace.table, (*declared types*)
   17.39 +    types: ((decl * Properties.T) * serial) NameSpace.table, (*declared types*)
   17.40      log_types: string list};                (*logical types sorted by number of arguments*)
   17.41  
   17.42  fun rep_tsig (TSig comps) = comps;