# 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')