src/HOL/Tools/datatype_abs_proofs.ML

       ||> Theory.checkpoint;
 
     val case_thms = map (map (fn t => SkipProof.prove_global thy2 [] [] t
       (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))
           (DatatypeProp.make_cases new_type_names descr sorts thy2)
-
   in
     thy2
+    |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
+       o Context.Theory
     |> parent_path flat_names
     |> store_thmss "cases" new_type_names case_thms
     |-> (fn thmss => pair (thmss, case_names))
   end;