src/Pure/General/properties.ML
changeset 50842 777c6026ca93
parent 46830 224d01fec36d
child 51665 cba83c9f72b9
--- a/src/Pure/General/properties.ML	Fri Jan 11 22:38:12 2013 +0100
+++ b/src/Pure/General/properties.ML	Sat Jan 12 14:47:17 2013 +0100
@@ -6,17 +6,19 @@
 
 signature PROPERTIES =
 sig
-  type T = (string * string) list
+  type entry = string * string
+  type T = entry list
   val defined: T -> string -> bool
   val get: T -> string -> string option
-  val put: string * string -> T -> T
+  val put: entry -> T -> T
   val remove: string -> T -> T
 end;
 
 structure Properties: PROPERTIES =
 struct
 
-type T = (string * string) list;
+type entry = string * string;
+type T = entry list;
 
 fun defined (props: T) name = AList.defined (op =) props name;
 fun get (props: T) name = AList.lookup (op =) props name;