--- a/src/HOL/Tools/datatype_package.ML Wed Jul 10 16:54:07 2002 +0200
+++ b/src/HOL/Tools/datatype_package.ML Wed Jul 10 18:35:34 2002 +0200
@@ -548,7 +548,7 @@
thy2 |>
Theory.add_path (space_implode "_" new_type_names) |>
PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
- [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>>
+ [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 |>>>