1.1 --- a/src/HOL/Tools/ctr_sugar.ML	Sat Dec 07 13:10:56 2013 +0100
     1.2 +++ b/src/HOL/Tools/ctr_sugar.ML	Sat Dec 07 18:06:49 2013 +0100
     1.3 @@ -930,11 +930,14 @@
     1.4              Local_Theory.declaration {syntax = false, pervasive = true}
     1.5                (fn phi => Case_Translation.register
     1.6                   (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
     1.7 -         |> (not no_code andalso null (Thm.hyps_of (hd case_thms)))
     1.8 -           ? Local_Theory.background_theory
     1.9 -               (fold (fold Code.del_eqn) [disc_defs, sel_defs]
    1.10 -                #> add_ctr_code fcT_name As (map dest_Const ctrs) inject_thms distinct_thms
    1.11 -                  case_thms)
    1.12 +         |> Local_Theory.background_theory (fold (fold Code.del_eqn) [disc_defs, sel_defs])
    1.13 +         |> not no_code ?
    1.14 +            Local_Theory.declaration {syntax = false, pervasive = false}
    1.15 +              (fn phi => Context.mapping
    1.16 +                (add_ctr_code fcT_name (map (Morphism.typ phi) As)
    1.17 +                  (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
    1.18 +                  (Morphism.fact phi distinct_thms) (Morphism.fact phi case_thms))
    1.19 +                I)
    1.20           |> Local_Theory.notes (anonymous_notes @ notes) |> snd
    1.21           |> register_ctr_sugar fcT_name ctr_sugar)
    1.22        end;

     2.1 --- a/src/HOL/Tools/ctr_sugar_code.ML	Sat Dec 07 13:10:56 2013 +0100
     2.2 +++ b/src/HOL/Tools/ctr_sugar_code.ML	Sat Dec 07 18:06:49 2013 +0100
     2.3 @@ -110,8 +110,10 @@
     2.4      #> snd
     2.5    end;
     2.6  
     2.7 -fun add_ctr_code fcT_name As ctrs inject_thms distinct_thms case_thms thy =
     2.8 +fun add_ctr_code fcT_name raw_As raw_ctrs inject_thms distinct_thms case_thms thy =
     2.9    let
    2.10 +    val As = map (perhaps (try Logic.unvarifyT_global)) raw_As;
    2.11 +    val ctrs = map (apsnd (perhaps (try Logic.unvarifyT_global))) raw_ctrs;
    2.12      val fcT = Type (fcT_name, As);
    2.13      val unover_ctrs = map (fn ctr as (_, fcT) => (Axclass.unoverload_const thy ctr, fcT)) ctrs;
    2.14    in