1.1 --- a/src/HOL/Tools/ctr_sugar.ML	Thu Dec 05 14:11:45 2013 +0100
     1.2 +++ b/src/HOL/Tools/ctr_sugar.ML	Thu Dec 05 14:35:58 2013 +0100
     1.3 @@ -930,11 +930,13 @@
     1.4              Local_Theory.declaration {syntax = false, pervasive = true}
     1.5                (fn phi => Case_Translation.register
     1.6                   (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
     1.7 -         |> Local_Theory.notes (anonymous_notes @ notes) |> snd
     1.8 -         |> register_ctr_sugar fcT_name ctr_sugar
     1.9           |> (not no_code andalso null (Thm.hyps_of (hd case_thms)))
    1.10             ? Local_Theory.background_theory
    1.11 -             (add_ctr_code fcT_name As (map dest_Const ctrs) inject_thms distinct_thms case_thms))
    1.12 +               (fold (fold Code.del_eqn) [disc_defs, sel_defs]
    1.13 +                #> add_ctr_code fcT_name As (map dest_Const ctrs) inject_thms distinct_thms
    1.14 +                  case_thms)
    1.15 +         |> Local_Theory.notes (anonymous_notes @ notes) |> snd
    1.16 +         |> register_ctr_sugar fcT_name ctr_sugar)
    1.17        end;
    1.18    in
    1.19      (goalss, after_qed, lthy')