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