
diff -r a6eeca90fd4e -r 1dedc0b76f32 Nominal/LFex.thy
--- a/Nominal/LFex.thy	Thu Feb 25 09:41:14 2010 +0100
+++ b/Nominal/LFex.thy	Thu Feb 25 12:15:11 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}, []),




