src/HOL/Tools/Datatype/rep_datatype.ML

         ((Binding.empty, [Induct.induct_simp_add]), [(flat (distinct @ inject), [])])] @
           named_rules @ unnamed_rules)
     |> snd
     |> Datatype_Data.register dt_infos
     |> Datatype_Data.interpretation_data (config, dt_names)
-    |> Datatype_Case.add_case_tr' case_names
     |> pair dt_names
   end;
 
 end;