--- a/src/Pure/General/properties.ML Wed Mar 07 19:32:52 2012 +0100
+++ b/src/Pure/General/properties.ML Wed Mar 07 19:38:36 2012 +0100
@@ -6,19 +6,17 @@
signature PROPERTIES =
sig
- type entry = string * string
- type T = entry list
+ type T = (string * string) list
val defined: T -> string -> bool
val get: T -> string -> string option
- val put: entry -> T -> T
+ val put: string * string -> T -> T
val remove: string -> T -> T
end;
structure Properties: PROPERTIES =
struct
-type entry = string * string;
-type T = entry list;
+type T = (string * string) list;
fun defined (props: T) name = AList.defined (op =) props name;
fun get (props: T) name = AList.lookup (op =) props name;
--- a/src/Pure/more_thm.ML Wed Mar 07 19:32:52 2012 +0100
+++ b/src/Pure/more_thm.ML Wed Mar 07 19:38:36 2012 +0100
@@ -79,9 +79,9 @@
val proof_attributes: attribute list -> thm -> Proof.context -> thm * Proof.context
val no_attributes: 'a -> 'a * 'b list
val simple_fact: 'a -> ('a * 'b list) list
- val tag_rule: Properties.entry -> thm -> thm
+ val tag_rule: string * string -> thm -> thm
val untag_rule: string -> thm -> thm
- val tag: Properties.entry -> attribute
+ val tag: string * string -> attribute
val untag: string -> attribute
val def_name: string -> string
val def_name_optional: string -> string -> string