src/Pure/Isar/induct_attrib.ML

   val find_casesS: Proof.context -> term -> thm list
   val find_inductT: Proof.context -> typ -> thm list
   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
   val typeN: string
   val setN: string

 
 end;
 
 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")]);
-
-end;
+  [(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;