src/HOL/Tools/datatype_rep_proofs.ML

             DEPTH_SOLVE_1 (ares_tac [prem] 1)]))
               (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
 
     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)
   end;