src/HOL/Tools/Datatype/datatype.ML

              [REPEAT (eresolve_tac Abs_inverse_thms 1),
               simp_tac (HOL_basic_ss addsimps (Thm.symmetric r :: Rep_inverse_thms')) 1,
               DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
                   (prems ~~ (constr_defs @ map mk_meta_eq iso_char_thms)))]);
 
-    val ([dt_induct'], thy7) =
+    val ([(_, [dt_induct'])], thy7) =
       thy6
-      |> Global_Theory.add_thms
-        [((Binding.qualify true big_name (Binding.name "induct"), dt_induct),
-          [case_names_induct])]
+      |> Global_Theory.note_thmss ""
+        [((Binding.qualify true big_name (Binding.name "induct"), [case_names_induct]),
+          [([dt_induct], [])])]
       ||> Theory.checkpoint;
 
   in
     ((constr_inject', distinct_thms', dt_induct'), thy7)
   end;