diff -r b0eae8c93314 -r da44ef9a7df2 Nominal/LFex.thy
--- a/Nominal/LFex.thy	Tue Mar 02 16:03:19 2010 +0100
+++ b/Nominal/LFex.thy	Tue Mar 02 16:04:48 2010 +0100
@@ -45,11 +45,10 @@
 done
 
 lemma alpha_eqvt:
-  "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)"
-  "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)"
-  "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)"
-apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts)
-apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros)
+  "(t1 \<approx>ki s1 \<longrightarrow> (p \<bullet> t1) \<approx>ki (p \<bullet> s1)) \<and>
+   (t2 \<approx>ty s2 \<longrightarrow> (p \<bullet> t2) \<approx>ty (p \<bullet> s2)) \<and>
+   (t3 \<approx>tr s3 \<longrightarrow> (p \<bullet> t3) \<approx>tr (p \<bullet> s3))"
+apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct)
 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj)
 apply (erule alpha_gen_compose_eqvt)
 apply (simp_all add: rfv_eqvt eqvts atom_eqvt)