# HG changeset patch
# User traytel
# Date 1386436009 -3600
# Node ID 506312c293f53fa93b6f85ddb87c214c1defe1cc
# Parent  cd88b44623bf28bdaec616becbaee92561475ac0
code equations for "local" (co)datatypes available after interpretation of locales with assumptions

diff -r cd88b44623bf -r 506312c293f5 src/HOL/Tools/ctr_sugar.ML
--- a/src/HOL/Tools/ctr_sugar.ML	Sat Dec 07 13:10:56 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar.ML	Sat Dec 07 18:06:49 2013 +0100
@@ -930,11 +930,14 @@
             Local_Theory.declaration {syntax = false, pervasive = true}
               (fn phi => Case_Translation.register
                  (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
-         |> (not no_code andalso null (Thm.hyps_of (hd case_thms)))
-           ? Local_Theory.background_theory
-               (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.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs])
+         |> not no_code ?
+            Local_Theory.declaration {syntax = false, pervasive = false}
+              (fn phi => Context.mapping
+                (add_ctr_code fcT_name (map (Morphism.typ phi) As)
+                  (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
+                  (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
+                I)
          |> Local_Theory.notes (anonymous_notes @ notes) |> snd
          |> register_ctr_sugar fcT_name ctr_sugar)
       end;
diff -r cd88b44623bf -r 506312c293f5 src/HOL/Tools/ctr_sugar_code.ML
--- a/src/HOL/Tools/ctr_sugar_code.ML	Sat Dec 07 13:10:56 2013 +0100
+++ b/src/HOL/Tools/ctr_sugar_code.ML	Sat Dec 07 18:06:49 2013 +0100
@@ -110,8 +110,10 @@
     #> snd
   end;
 
-fun add_ctr_code fcT_name As ctrs inject_thms distinct_thms case_thms thy =
+fun add_ctr_code fcT_name raw_As raw_ctrs inject_thms distinct_thms case_thms thy =
   let
+    val As = map (perhaps (try Logic.unvarifyT_global)) raw_As;
+    val ctrs = map (apsnd (perhaps (try Logic.unvarifyT_global))) raw_ctrs;
     val fcT = Type (fcT_name, As);
     val unover_ctrs = map (fn ctr as (_, fcT) => (Axclass.unoverload_const thy ctr, fcT)) ctrs;
   in