--- 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
@@ -66,6 +66,7 @@
open Ctr_Sugar_Util
open Ctr_Sugar_Tactics
+open Ctr_Sugar_Code
type ctr_sugar =
{ctrs: term list,
@@ -926,11 +927,13 @@
(ctr_sugar,
lthy
|> not rep_compat ?
- (Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Case_Translation.register
- (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
+ 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)
+ |> 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))
end;
in
(goalss, after_qed, lthy')