diff -r 7b1a3df239cd -r 10a0e3578507 Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Mon Feb 22 14:50:53 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Mon Feb 22 15:03:48 2010 +0100
@@ -185,15 +185,12 @@
   apply(induct K K' and A A' and M M' rule: akind_aty_atrm.inducts)
   apply(simp_all add: akind_aty_atrm.intros)
   apply (simp_all add: akind_aty_atrm_inj)
-  apply(rule alpha_gen_atom_sym)
-  apply(rule alpha_eqvt)
-  apply(assumption)+
-  apply(rule alpha_gen_atom_sym)
-  apply(rule alpha_eqvt)
-  apply(assumption)+
-  apply(rule alpha_gen_atom_sym)
-  apply(rule alpha_eqvt)
-  apply(assumption)+
+  apply(erule alpha_gen_compose_sym)
+  apply(erule alpha_eqvt)
+  apply(erule alpha_gen_compose_sym)
+  apply(erule alpha_eqvt)
+  apply(erule alpha_gen_compose_sym)
+  apply(erule alpha_eqvt)
   done
 
 lemma al_trans:
@@ -206,9 +203,9 @@
   apply(erule akind.cases)
   apply(simp_all add: akind_aty_atrm.intros)
   apply(simp add: akind_aty_atrm_inj)
-  apply(rule alpha_gen_atom_trans)
-  apply(rule alpha_eqvt)
-  apply(assumption)+
+  apply(erule alpha_gen_compose_trans)
+  apply(assumption)
+  apply(erule alpha_eqvt)
   apply(rotate_tac 4)
   apply(erule aty.cases)
   apply(simp_all add: akind_aty_atrm.intros)
@@ -216,9 +213,9 @@
   apply(erule aty.cases)
   apply(simp_all add: akind_aty_atrm.intros)
   apply(simp add: akind_aty_atrm_inj)
-  apply(rule alpha_gen_atom_trans)
-  apply(rule alpha_eqvt)
-  apply(assumption)+
+  apply(erule alpha_gen_compose_trans)
+  apply(assumption)
+  apply(erule alpha_eqvt)
   apply(rotate_tac 4)
   apply(erule atrm.cases)
   apply(simp_all add: akind_aty_atrm.intros)
@@ -226,9 +223,9 @@
   apply(erule atrm.cases)
   apply(simp_all add: akind_aty_atrm.intros)
   apply(simp add: akind_aty_atrm_inj)
-  apply(rule alpha_gen_atom_trans)
-  apply(rule alpha_eqvt)
-  apply(assumption)+
+  apply(erule alpha_gen_compose_trans)
+  apply(assumption)
+  apply(erule alpha_eqvt)
   done
 
 lemma alpha_equivps: