--- a/Quot/Nominal/Terms.thy	Mon Feb 22 14:50:53 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Mon Feb 22 15:03:48 2010 +0100
@@ -116,23 +116,6 @@
   apply(simp add: permute_eqvt[symmetric])
   done
 
-lemma alpha_gen_atom_sym:
-  assumes b: "\<exists>pi. (aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)"
-  and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))"
-  shows "\<exists>pi. (ab, s) \<approx>gen R f pi (aa, t)"
-  using b apply -
-  apply(erule exE)
-  apply(rule_tac x="- pi" in exI)
-  apply(simp add: alpha_gen.simps)
-  apply(erule conjE)+
-  apply(rule conjI)
-  apply(simp add: fresh_star_def fresh_minus_perm)
-  apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))")
-  apply simp
-  apply(rule a)
-  apply assumption
-  done
-
 prove alpha1_reflp_aux: {* fst (build_alpha_refl_gl [@{term alpha_rtrm1}, @{term alpha_bp}]) *}
 by (tactic {*
 
@@ -148,7 +131,7 @@
  (rtac @{thm alpha_rtrm1_alpha_bp.induct} THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_inj}) THEN_ALL_NEW
   TRY o REPEAT_ALL_NEW (CHANGED o rtac @{thm conjI}) THEN_ALL_NEW
- (etac @{thm alpha_gen_atom_sym} THEN'
+ (etac @{thm alpha_gen_compose_sym} THEN'
   asm_full_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt})
  )) 1 *})
 
@@ -163,7 +146,7 @@
 apply (rotate_tac 2)
 apply (erule alpha_rtrm1.cases)
 apply (simp_all add: alpha1_inj)
-thm alpha_gen_atom_trans
+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 *})*)