src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 55471 198498f861ee
parent 55470 46e6e1d91056
child 55480 59cc4a8bc28a
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Feb 14 07:53:46 2014 +0100
     1.3 @@ -941,8 +941,10 @@
     1.4          (ctr_sugar,
     1.5           lthy
     1.6           |> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms)
     1.7 -         |> Spec_Rules.add Spec_Rules.Equational (flat selss, all_sel_thms)
     1.8 -         |> fold (Spec_Rules.add Spec_Rules.Equational) (map single discs ~~ nontriv_disc_eq_thmss)
     1.9 +         |> fold (Spec_Rules.add Spec_Rules.Equational)
    1.10 +           (AList.group (eq_list (op aconv)) (map (`lhs_heads_of) all_sel_thms))
    1.11 +         |> fold (Spec_Rules.add Spec_Rules.Equational)
    1.12 +           (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
    1.13           |> Local_Theory.declaration {syntax = false, pervasive = true}
    1.14                (fn phi => Case_Translation.register
    1.15                   (Morphism.term phi casex) (map (Morphism.term phi) ctrs))