--- a/src/Pure/more_thm.ML Sun Oct 25 19:18:25 2009 +0100
+++ b/src/Pure/more_thm.ML Sun Oct 25 19:18:59 2009 +0100
@@ -83,9 +83,6 @@
val has_name_hint: thm -> bool
val get_name_hint: thm -> string
val put_name_hint: string -> thm -> thm
- val get_group: thm -> string option
- val put_group: string -> thm -> thm
- val group: string -> attribute
val axiomK: string
val assumptionK: string
val definitionK: string
@@ -417,15 +414,6 @@
fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name);
-(* theorem groups *)
-
-fun get_group thm = Properties.get (Thm.get_tags thm) Markup.groupN;
-
-fun put_group name = if name = "" then I else Thm.map_tags (Properties.put (Markup.groupN, name));
-
-fun group name = rule_attribute (K (put_group name));
-
-
(* theorem kinds *)
val axiomK = "axiom";