--- a/Nominal/nominal_dt_alpha.ML	Thu Jun 16 23:11:50 2011 +0900
+++ b/Nominal/nominal_dt_alpha.ML	Thu Jun 16 20:07:03 2011 +0100
@@ -26,8 +26,9 @@
     (Proof.context -> int -> tactic) -> Proof.context -> thm list
 
   val raw_prove_refl: term list -> term list -> thm list -> thm -> Proof.context -> thm list
-  val raw_prove_sym: term list -> thm list -> thm -> Proof.context -> thm list
-  val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> Proof.context -> thm list
+  val raw_prove_sym: term list -> thm list -> thm -> thm list -> Proof.context -> thm list
+  val raw_prove_trans: term list -> thm list -> thm list -> thm -> thm list -> thm list -> 
+    Proof.context -> thm list
   val raw_prove_equivp: term list -> term list -> thm list -> thm list -> thm list -> 
     Proof.context -> thm list * thm list
 
@@ -492,7 +493,7 @@
   by (erule exE, rule_tac x="-p" in exI, auto)}
 
 (* for premises that contain binders *)
-fun prem_bound_tac pred_names ctxt = 
+fun prem_bound_tac pred_names alpha_eqvt ctxt = 
   let
     fun trans_prem_tac pred_names ctxt = 
       SUBPROOF (fn {prems, context, ...} => 
@@ -507,20 +508,20 @@
       [ etac exi_neg,
         resolve_tac @{thms alpha_sym_eqvt},
         asm_full_simp_tac (HOL_ss addsimps prod_simps),
-        eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl},
-        trans_prem_tac pred_names ctxt ] 
+        eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
+        trans_prem_tac pred_names ctxt] 
   end
 
-fun raw_prove_sym alpha_trms alpha_intros alpha_induct ctxt =
+fun raw_prove_sym alpha_trms alpha_intros alpha_induct alpha_eqvt ctxt =
   let
     val props = map (fn t => fn (x, y) => t $ y $ x) alpha_trms
-  
+
     fun tac ctxt = 
       let
         val alpha_names =  map (fst o dest_Const) alpha_trms   
       in
         resolve_tac alpha_intros THEN_ALL_NEW 
-        FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names ctxt]
+        FIRST' [atac, rtac @{thm sym} THEN' atac, prem_bound_tac alpha_names alpha_eqvt ctxt]
     end
   in
     alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct tac ctxt 
@@ -549,7 +550,7 @@
       HEADGOAL (rtac exi_inst)
     end)
 
-fun non_trivial_cases_tac pred_names intros ctxt = 
+fun non_trivial_cases_tac pred_names intros alpha_eqvt ctxt = 
   let
     val prod_simps = @{thms split_conv alphas permute_prod.simps prod_alpha_def prod_rel_def}
   in
@@ -562,15 +563,15 @@
           resolve_tac @{thms alpha_trans_eqvt}, 
           atac,
           aatac pred_names ctxt, 
-          eqvt_tac ctxt eqvt_relaxed_config THEN' rtac @{thm refl},
+          eqvt_tac ctxt (eqvt_relaxed_config addpres alpha_eqvt) THEN' rtac @{thm refl},
           asm_full_simp_tac (HOL_ss addsimps prod_simps) ])
   end
 			  
-fun prove_trans_tac pred_names raw_dt_thms intros cases ctxt =
+fun prove_trans_tac pred_names raw_dt_thms intros cases alpha_eqvt ctxt =
   let
     fun all_cases ctxt = 
       asm_full_simp_tac (HOL_basic_ss addsimps raw_dt_thms) 
-      THEN' TRY o non_trivial_cases_tac pred_names intros ctxt
+      THEN' TRY o non_trivial_cases_tac pred_names intros alpha_eqvt ctxt
   in
     EVERY' [ rtac @{thm allI}, rtac @{thm impI}, 
              ecases_tac cases ctxt THEN_ALL_NEW all_cases ctxt ]
@@ -585,13 +586,13 @@
     HOLogic.all_const arg_ty $ Abs ("z", arg_ty, HOLogic.mk_imp (mid, rhs))
   end
 
-fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases ctxt =
+fun raw_prove_trans alpha_trms raw_dt_thms alpha_intros alpha_induct alpha_cases alpha_eqvt ctxt =
   let
     val alpha_names =  map (fst o dest_Const) alpha_trms 
     val props = map prep_trans_goal alpha_trms
   in
     alpha_prove alpha_trms (alpha_trms ~~ props) alpha_induct
-      (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases) ctxt
+      (prove_trans_tac alpha_names raw_dt_thms alpha_intros alpha_cases alpha_eqvt) ctxt
   end