src/HOL/Tools/datatype_package.ML
changeset 13340 9b0332344ae2
parent 12922 ed70a600f0ea
child 13462 56610e2ba220
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Jul 10 16:54:07 2002 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Jul 10 18:35:34 2002 +0200
     1.3 @@ -548,7 +548,7 @@
     1.4        thy2 |>
     1.5        Theory.add_path (space_implode "_" new_type_names) |>
     1.6        PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts),
     1.7 -        [Drule.rule_attribute (K InductivePackage.rulify), case_names_induct])] |>>>
     1.8 +        [case_names_induct])] |>>>
     1.9        PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>>
    1.10        (if no_size then I else #1 o PureThy.add_axiomss_i [(("size", size_axs), [])]) |>>
    1.11        Theory.parent_path |>>>