--- 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