1.1 --- a/src/HOL/Tools/ctr_sugar.ML	Mon Dec 02 20:31:54 2013 +0100
     1.2 +++ b/src/HOL/Tools/ctr_sugar.ML	Mon Dec 02 20:31:54 2013 +0100
     1.3 @@ -932,8 +932,9 @@
     1.4                   (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
     1.5           |> Local_Theory.notes (anonymous_notes @ notes) |> snd
     1.6           |> register_ctr_sugar fcT_name ctr_sugar
     1.7 -         |> Local_Theory.background_theory
     1.8 -           (add_ctr_code fcT_name As (map dest_Const ctrs) inject_thms distinct_thms case_thms))
     1.9 +         |> 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        end;
    1.13    in
    1.14      (goalss, after_qed, lthy')