--- a/Nominal/nominal_dt_alpha.ML	Sat Aug 14 23:33:23 2010 +0800
+++ b/Nominal/nominal_dt_alpha.ML	Sun Aug 15 11:03:13 2010 +0800
@@ -11,8 +11,8 @@
     bclause list list list -> term list -> Proof.context -> 
     term list * term list * thm list * thm list * thm * local_theory
 
-  val mk_alpha_distincts: Proof.context -> thm list -> thm list list -> 
-    term list -> term list -> bn_info -> thm list * thm list
+  val mk_alpha_distincts: Proof.context -> thm list -> thm list -> 
+    term list -> typ list -> thm list
 
   val mk_alpha_eq_iff: Proof.context -> thm list -> thm list -> thm list -> 
     thm list -> (thm list * thm list)
@@ -270,42 +270,41 @@
 
 (* transforms the distinctness theorems of the constructors 
    to "not-alphas" of the constructors *)
-fun mk_alpha_distinct_goal alpha neq =
+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
 in
-  alpha $ lhs $ rhs
+  (lookup ty_trm_assoc ty) $ lhs $ rhs
   |> HOLogic.mk_not
   |> HOLogic.mk_Trueprop
 end
 
-fun distinct_tac cases distinct_thms =
-  rtac notI THEN' eresolve_tac cases 
+fun distinct_tac cases_thms distinct_thms =
+  rtac notI THEN' eresolve_tac cases_thms 
   THEN_ALL_NEW asm_full_simp_tac (HOL_ss addsimps distinct_thms)
 
-fun mk_alpha_distinct ctxt cases_thms (distinct_thm, alpha) =
+
+fun mk_alpha_distincts ctxt cases_thms distinct_thms alpha_trms alpha_tys =
 let
-  val ((_, thms), ctxt') = Variable.import false distinct_thm ctxt
-  val goals = map (mk_alpha_distinct_goal alpha o prop_of) thms
-  val nrels = map (fn t => Goal.prove ctxt' [] [] t (K (distinct_tac cases_thms distinct_thm 1))) goals
-in
-  Variable.export ctxt' ctxt nrels
-end
+  val ty_trm_assoc = alpha_tys ~~ alpha_trms
 
-fun mk_alpha_distincts ctxt alpha_cases constrs_distinct_thms alpha_trms alpha_bn_trms bn_infos =
-let
-  val alpha_distincts = 
-    map (mk_alpha_distinct ctxt alpha_cases) (constrs_distinct_thms ~~ alpha_trms)
-  val distinc_thms = map 
-  val alpha_bn_distincts_aux = map (fn (_, i, _) => nth constrs_distinct_thms i) bn_infos
-  val alpha_bn_distincts =  
-    map (mk_alpha_distinct ctxt alpha_cases) (alpha_bn_distincts_aux ~~ alpha_bn_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'
+  in
+    Goal.prove ctxt' [] [] goal 
+      (K (distinct_tac cases_thms distinct_thms 1))
+    |> singleton (Variable.export ctxt' ctxt)
+  end
+    
 in
-  (flat alpha_distincts, flat alpha_bn_distincts)
+  map (mk_alpha_distinct o prop_of) distinct_thms
 end
 
 
@@ -692,7 +691,7 @@
 end
 
 
-(* transformation of the natural rsp-lemmas into the standard form *)
+(* transformation of the natural rsp-lemmas into standard form *)
 
 val fun_rsp = @{lemma
   "(!x y. R x y --> f x = f y) ==> (R ===> (op =)) f f" by simp}