src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 55535 10194808430d
parent 55480 59cc4a8bc28a
child 56345 228e30cb111d
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Feb 17 13:31:42 2014 +0100
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Feb 17 13:31:42 2014 +0100
     1.3 @@ -942,7 +942,7 @@
     1.4           lthy
     1.5           |> Spec_Rules.add Spec_Rules.Equational ([casex], case_thms)
     1.6           |> fold (Spec_Rules.add Spec_Rules.Equational)
     1.7 -           (AList.group (eq_list (op aconv)) (map (`lhs_heads_of) all_sel_thms))
     1.8 +           (AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms))
     1.9           |> fold (Spec_Rules.add Spec_Rules.Equational)
    1.10             (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
    1.11           |> Local_Theory.declaration {syntax = false, pervasive = true}