--- a/LFex.thy	Sun Dec 06 11:39:34 2009 +0100
+++ b/LFex.thy	Sun Dec 06 13:41:42 2009 +0100
@@ -258,7 +258,7 @@
 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
 apply - 
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
-apply(tactic {* regularize_tac @{context} @{thms alpha_equivps} 1 *})
+apply(tactic {* regularize_tac @{context} 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})
 apply(fold perm_kind_def perm_ty_def perm_trm_def)
 apply(tactic {* clean_tac @{context} 1 *})
@@ -296,7 +296,7 @@
   \<And>trm1 trm2. \<lbrakk>P3 trm1; P3 trm2\<rbrakk> \<Longrightarrow> P3 (APP trm1 trm2);
   \<And>ty name trm. \<lbrakk>P2 ty; P3 trm\<rbrakk> \<Longrightarrow> P3 (LAM ty name trm)\<rbrakk>
   \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 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