# HG changeset patch
# User wenzelm
# Date 1331145516 -3600
# Node ID 224d01fec36d5693fcc85c4efbc776214b0b8778
# Parent  9770573e2172018681434cefdbfb0bdd8a0fb496
tuned signature;

diff -r 9770573e2172 -r 224d01fec36d src/Pure/General/properties.ML
--- 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;
diff -r 9770573e2172 -r 224d01fec36d src/Pure/more_thm.ML
--- 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