# HG changeset patch
# User blanchet
# Date 1386250558 -3600
# Node ID 30666a281ae3b317dce4c0b70fb3772da863fedd
# Parent  36629751709126b882fbe0d6a88193b9bb239f53
proper code generation for discriminators/selectors

diff -r 366297517091 -r 30666a281ae3 src/HOL/Tools/ctr_sugar.ML
--- a/src/HOL/Tools/ctr_sugar.ML	Thu Dec 05 14:11:45 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar.ML	Thu Dec 05 14:35:58 2013 +0100
@@ -930,11 +930,13 @@
             Local_Theory.declaration {syntax = false, pervasive = true}
               (fn phi => Case_Translation.register
                  (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
-         |> Local_Theory.notes (anonymous_notes @ notes) |> snd
-         |> register_ctr_sugar fcT_name ctr_sugar
          |> (not no_code andalso null (Thm.hyps_of (hd case_thms)))
            ? Local_Theory.background_theory
-             (add_ctr_code fcT_name As (map dest_Const ctrs) inject_thms distinct_thms case_thms))
+               (fold (fold Code.del_eqn) [disc_defs, sel_defs]
+                #> add_ctr_code fcT_name As (map dest_Const ctrs) inject_thms distinct_thms
+                  case_thms)
+         |> Local_Theory.notes (anonymous_notes @ notes) |> snd
+         |> register_ctr_sugar fcT_name ctr_sugar)
       end;
   in
     (goalss, after_qed, lthy')