diff -r b0a120469041 -r 70c2cde06c4e Nominal/LFex.thy
--- a/Nominal/LFex.thy	Thu Feb 25 11:51:34 2010 +0100
+++ b/Nominal/LFex.thy	Thu Feb 25 12:24:37 2010 +0100
@@ -51,15 +51,12 @@
 apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
-apply (rule alpha_gen_atom_eqvt)
-apply (simp add: rfv_eqvt)
-apply assumption
-apply (rule alpha_gen_atom_eqvt)
-apply (simp add: rfv_eqvt)
-apply assumption
-apply (rule alpha_gen_atom_eqvt)
-apply (simp add: rfv_eqvt)
-apply assumption
+apply (erule alpha_gen_compose_eqvt)
+apply (simp_all add: rfv_eqvt eqvts atom_eqvt)
+apply (erule alpha_gen_compose_eqvt)
+apply (simp_all add: rfv_eqvt eqvts atom_eqvt)
+apply (erule alpha_gen_compose_eqvt)
+apply (simp_all add: rfv_eqvt eqvts atom_eqvt)
 done
 
 local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_equivps}, []),