src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML

            sel_split_asms = sel_split_asm_thms, case_eq_ifs = case_eq_if_thms};
       in
         (ctr_sugar,
          lthy
          |> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms)
-         |> Spec_Rules.add Spec_Rules.Equational (flat selss, all_sel_thms)
-         |> fold (Spec_Rules.add Spec_Rules.Equational) (map single discs ~~ nontriv_disc_eq_thmss)
+         |> fold (Spec_Rules.add Spec_Rules.Equational)
+           (AList.group (eq_list (op aconv)) (map (`lhs_heads_of) all_sel_thms))
+         |> fold (Spec_Rules.add Spec_Rules.Equational)
+           (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
          |> Local_Theory.declaration {syntax = false, pervasive = true}
               (fn phi => Case_Translation.register
                  (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
          |> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs])
          |> not no_code ?