src/HOL/Tools/datatype_package.ML
changeset 10911 eb5721204b38
parent 10525 3e21ab3e5114
child 10930 7c7a7b0e1d0c
--- a/src/HOL/Tools/datatype_package.ML	Tue Jan 16 00:32:38 2001 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Tue Jan 16 00:33:40 2001 +0100
@@ -532,7 +532,8 @@
     val (thy3, (([induct], [rec_thms]), inject)) =
       thy2 |>
       Theory.add_path (space_implode "_" new_type_names) |>
-      PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [case_names_induct])] |>>>
+      PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
+        [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>>
       PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>>
       (if no_size then I else #1 o PureThy.add_axiomss_i [(("size", size_axs), [])]) |>>
       Theory.parent_path |>>>