# HG changeset patch
# User blanchet
# Date 1386012714 -3600
# Node ID 1183bd5119800a1c1fbec0996067e41b3a10568f
# Parent  a21a2223c02b0e7e581b56f77e820d08f401c998
don't try to register code equations in a locale with assumptions

diff -r a21a2223c02b -r 1183bd511980 src/HOL/Tools/ctr_sugar.ML
--- a/src/HOL/Tools/ctr_sugar.ML	Mon Dec 02 20:31:54 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar.ML	Mon Dec 02 20:31:54 2013 +0100
@@ -932,8 +932,9 @@
                  (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
          |> Local_Theory.notes (anonymous_notes @ notes) |> snd
          |> register_ctr_sugar fcT_name ctr_sugar
-         |> Local_Theory.background_theory
-           (add_ctr_code fcT_name As (map dest_Const ctrs) inject_thms distinct_thms case_thms))
+         |> 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))
       end;
   in
     (goalss, after_qed, lthy')