--- a/src/Pure/Isar/induct_attrib.ML Fri Jan 20 04:53:59 2006 +0100
+++ b/src/Pure/Isar/induct_attrib.ML Sat Jan 21 23:02:14 2006 +0100
@@ -25,12 +25,12 @@
val find_inductS: Proof.context -> term -> thm list
val find_coinductT: Proof.context -> typ -> thm list
val find_coinductS: Proof.context -> term -> thm list
- val cases_type: string -> Context.generic attribute
- val cases_set: string -> Context.generic attribute
- val induct_type: string -> Context.generic attribute
- val induct_set: string -> Context.generic attribute
- val coinduct_type: string -> Context.generic attribute
- val coinduct_set: string -> Context.generic attribute
+ val cases_type: string -> attribute
+ val cases_set: string -> attribute
+ val induct_type: string -> attribute
+ val induct_set: string -> attribute
+ val coinduct_type: string -> attribute
+ val coinduct_set: string -> attribute
val casesN: string
val inductN: string
val coinductN: string
@@ -225,8 +225,8 @@
val _ = Context.add_setup
(Attrib.add_attributes
- [(casesN, Attrib.common cases_att, "declaration of cases rule for type or set"),
- (inductN, Attrib.common induct_att, "declaration of induction rule for type or set"),
- (coinductN, Attrib.common coinduct_att, "declaration of coinduction rule for type or set")]);
+ [(casesN, cases_att, "declaration of cases rule for type or set"),
+ (inductN, induct_att, "declaration of induction rule for type or set"),
+ (coinductN, coinduct_att, "declaration of coinduction rule for type or set")]);
end;