diff -r 97f6e5c61f03 -r cdc6ae1a4ed2 LFex.thy
--- a/LFex.thy	Sun Dec 06 23:35:02 2009 +0100
+++ b/LFex.thy	Mon Dec 07 00:07:23 2009 +0100
@@ -296,7 +296,7 @@
   \<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2);
   \<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk>
   \<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm"
-apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_equivps} 1 *})
+apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *})
 done
 
 print_quotients