--- a/Nominal/nominal_dt_alpha.ML	Sun Aug 22 14:02:49 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Wed Aug 25 09:02:06 2010 +0800
@@ -240,7 +240,7 @@
   val all_alpha_names = map (fn (a, ty) => ((Binding.name a, ty), NoSyn))
     (alpha_names @ alpha_bn_names ~~ alpha_tys @ alpha_bn_tys)
   val all_alpha_intros = map (pair Attrib.empty_binding) (flat alpha_intros @ flat alpha_bn_intros)
-  
+
   val (alphas, lthy') = Inductive.add_inductive_i
      {quiet_mode = true, verbose = false, alt_name = Binding.empty,
       coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
@@ -252,12 +252,13 @@
   val alpha_cases_loc = #elims alphas;
   val phi = ProofContext.export_morphism lthy' lthy;
 
-  val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc;
+  val all_alpha_trms = map (Morphism.term phi) all_alpha_trms_loc
+  val (all_alpha_trms', _) = Variable.importT_terms all_alpha_trms lthy  
   val alpha_induct = Morphism.thm phi alpha_induct_loc;
   val alpha_intros = map (Morphism.thm phi) alpha_intros_loc
   val alpha_cases = map (Morphism.thm phi) alpha_cases_loc
 
-  val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms
+  val (alpha_trms, alpha_bn_trms) = chop (length fvs) all_alpha_trms'
 in
   (alpha_trms, alpha_bn_trms, alpha_intros, alpha_cases, alpha_induct, lthy')
 end
@@ -289,12 +290,16 @@
 
 fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys =
 let
+  (* proper import of type-variables does not work,
+     since ther are replaced by new variables, messing
+     up the ty_term assoc list *)
+  val distinct_thms' = map Thm.legacy_freezeT distinct_thms
   val ty_trm_assoc = alpha_tys ~~ alpha_trms
 
   fun mk_alpha_distinct distinct_trm =
   let
     val ([trm'], ctxt') = Variable.import_terms true [distinct_trm] ctxt
-    val goal = mk_distinct_goal ty_trm_assoc trm'
+    val goal = mk_distinct_goal ty_trm_assoc distinct_trm
   in
     Goal.prove ctxt' [] [] goal 
       (K (distinct_tac cases_thms distinct_thms 1))
@@ -302,7 +307,8 @@
   end
     
 in
-  map (mk_alpha_distinct o prop_of) distinct_thms
+  map (mk_alpha_distinct o prop_of) distinct_thms'
+  |> map Thm.varifyT_global
 end