src/HOL/Tools/datatype_rep_proofs.ML
changeset 6092 d9db67970c73
parent 5696 c2c2214f8037
child 6171 cd237a10cbf8
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jan 12 13:40:08 1999 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Tue Jan 12 13:54:51 1999 +0100
     1.3 @@ -535,7 +535,7 @@
     1.4  
     1.5      val thy7 = thy6 |>
     1.6        Theory.add_path big_name |>
     1.7 -      PureThy.add_tthms [(("induct", Attribute.tthm_of dt_induct), [])] |>
     1.8 +      PureThy.add_thms [(("induct", dt_induct), [])] |>
     1.9        Theory.parent_path;
    1.10  
    1.11    in (thy7, constr_inject, dist_rewrites, dt_induct)