--- a/Nominal/nominal_dt_alpha.ML	Wed Jun 22 14:14:54 2011 +0100
+++ b/Nominal/nominal_dt_alpha.ML	Thu Jun 23 11:30:39 2011 +0100
@@ -14,7 +14,7 @@
     term list * term list * thm list * thm list * thm * local_theory
 
   val mk_alpha_distincts: Proof.context -> thm list -> thm list -> 
-    term list -> typ list -> thm list
+    term list -> string list -> thm list
 
   val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> 
     thm list -> thm list
@@ -262,14 +262,15 @@
     val alpha_intros_loc = #intrs alphas;
     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', _) = Variable.importT_terms all_alpha_trms lthy  
-    val alpha_induct = Morphism.thm phi alpha_induct_loc;
+    
+    val all_alpha_trms = all_alpha_trms_loc
+      |> map (Morphism.term phi) 
+      |> map Type.legacy_freeze 
+    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
@@ -279,17 +280,14 @@
 (** produces the distinctness theorems **)
 
 (* transforms the distinctness theorems of the constructors 
-   to "not-alphas" of the constructors *)
+   into "not-alphas" of the constructors *)
 fun mk_distinct_goal ty_trm_assoc neq =
   let
-    val (lhs, rhs) = 
-      neq
-      |> HOLogic.dest_Trueprop
-      |> HOLogic.dest_not
-      |> HOLogic.dest_eq
-    val ty = fastype_of lhs
+    val (Const (@{const_name "HOL.eq"}, ty_eq) $ lhs $ rhs) = 
+      HOLogic.dest_not (HOLogic.dest_Trueprop neq)
+    val ty_str = fst (dest_Type (domain_type ty_eq))
   in
-    (lookup ty_trm_assoc ty) $ lhs $ rhs
+    Const (lookup ty_trm_assoc ty_str, ty_eq) $ lhs $ rhs
     |> HOLogic.mk_not
     |> HOLogic.mk_Trueprop
   end
@@ -299,27 +297,19 @@
   THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)
 
 
-fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys =
+fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_str =
   let
-    (* proper import of type-variables does not work,
-       since then they are replaced by new variables, messing
-       up the ty_trm assoc list *)
-    val distinct_thms' = map Thm.legacy_freezeT distinct_thms
-    val ty_trm_assoc = alpha_tys ~~ alpha_trms
+    val ty_trm_assoc = alpha_str ~~ (map (fst o dest_Const) 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 distinct_trm
     in
-      Goal.prove ctxt' [] [] goal 
+      Goal.prove ctxt [] [] goal 
         (K (distinct_tac cases_thms distinct_thms 1))
-      |> singleton (Variable.export ctxt' ctxt)
     end
-    
   in
-    map (mk_alpha_distinct o prop_of) distinct_thms'
-    |> map Thm.varifyT_global
+    map (mk_alpha_distinct o prop_of) distinct_thms
   end
 
 
@@ -657,17 +647,16 @@
 
 fun raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms fvs bns fv_bns alpha_induct simps ctxt =
   let
-    val arg_ty = domain_type o fastype_of 
+    val arg_ty = fst o dest_Type o domain_type o fastype_of 
     val ty_assoc = map (fn t => (arg_ty t, t)) alpha_trms
     fun mk_eq' t x y = HOLogic.mk_eq (t $ x, t $ y)
 
     val prop1 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) fvs
     val prop2 = map (fn t => (lookup ty_assoc (arg_ty t), fn (x, y) => mk_eq' t x y)) (bns @ fv_bns)
     val prop3 = map2 (fn t1 => fn t2 => (t1, fn (x, y) => mk_eq' t2 x y)) alpha_bn_trms fv_bns
-  
+
     val ss = HOL_ss addsimps (simps @ @{thms alphas prod_fv.simps set.simps append.simps} 
       @ @{thms Un_assoc Un_insert_left Un_empty_right Un_empty_left}) 
-
   in
     alpha_prove (alpha_trms @ alpha_bn_trms) (prop1 @ prop2 @ prop3) alpha_induct 
       (K (asm_full_simp_tac ss)) ctxt
@@ -708,7 +697,6 @@
     THEN_ALL_NEW (TRY o (rtac exi_zero) THEN' asm_full_simp_tac post_ss)
   end
 
-
 fun raw_constrs_rsp constrs alpha_trms alpha_intros simps ctxt =
   let
     val alpha_arg_tys = map (domain_type o fastype_of) alpha_trms
@@ -718,15 +706,15 @@
         NONE => HOLogic.eq_const ty
       | SOME alpha => alpha 
   
-    fun fun_rel_app t1 t2 = 
+    fun fun_rel_app (t1, t2) = 
       Const (@{const_name "fun_rel"}, dummyT) $ t1 $ t2
 
     fun prep_goal trm =
       trm
       |> strip_type o fastype_of
-      |>> map lookup
-      ||> lookup
-      |> uncurry (fold_rev fun_rel_app)
+      |> (fn (tys, ty) => tys @ [ty])
+      |> map lookup
+      |> foldr1 fun_rel_app
       |> (fn t => t $ trm $ trm)
       |> Syntax.check_term ctxt
       |> HOLogic.mk_Trueprop