--- a/Quot/Nominal/LamEx2.thy	Mon Feb 22 14:50:53 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy	Mon Feb 22 15:03:48 2010 +0100
@@ -137,9 +137,8 @@
   apply(simp add: a1)
   apply(simp add: a2)
   apply(rule a3)
-  apply(rule alpha_gen_atom_sym)
-  apply(rule alpha_eqvt)
-  apply(assumption)+
+  apply(erule alpha_gen_compose_sym)
+  apply(erule alpha_eqvt)
   done
 
 lemma alpha_trans:
@@ -152,9 +151,9 @@
 apply(erule alpha.cases)
 apply(simp_all)
 apply(rule a3)
-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_equivp: