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