--- a/Quot/Nominal/Terms.thy	Mon Feb 22 15:09:53 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Mon Feb 22 15:41:30 2010 +0100
@@ -135,28 +135,24 @@
   asm_full_simp_tac (HOL_ss addsimps inj) THEN_ALL_NEW
   TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
   (etac @{thm alpha_gen_compose_sym} THEN'
-   asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}))
+   eresolve_tac @{thms alpha1_eqvt})
 *}
 
 prove alpha1_symp_aux: {* (fst o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
 by (tactic {* symp_tac @{thm alpha_rtrm1_alpha_bp.induct} @{thms alpha1_inj} 1 *})
 
 prove alpha1_transp_aux: {* (snd o snd) (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
-apply (rule alpha_rtrm1_alpha_bp.induct)
-apply simp_all
-apply (rule_tac [!] allI)
-apply (rule_tac [!] impI)
-apply (rotate_tac 4)
-apply (erule alpha_rtrm1.cases)
-apply (simp_all add: alpha1_inj)
-apply (rotate_tac 2)
-apply (erule alpha_rtrm1.cases)
-apply (simp_all add: alpha1_inj)
-apply (erule alpha_gen_compose_trans)
-(*apply (tactic {*
- (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW
-  asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj})) 1 *})*)
-sorry
+apply (tactic {*
+ (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW 
+  (rtac allI THEN' rtac impI THEN' rotate_tac (~1) THEN'
+  eresolve_tac @{thms alpha_rtrm1.cases alpha_bp.cases}) THEN_ALL_NEW
+  (
+    asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj rtrm1.distinct rtrm1.inject bp.distinct bp.inject}) THEN'
+    TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
+    (etac @{thm alpha_gen_compose_trans} THEN' RANGE [atac, eresolve_tac @{thms alpha1_eqvt}])
+  )
+) 1 *})
+done
 
 lemma helper: "(\<forall>x y z. R x y \<and> R y z \<longrightarrow> R x z) = (\<forall>xa ya. R xa ya \<longrightarrow> (\<forall>z. R ya z \<longrightarrow> R xa z))"
 by meson