--- a/LFex.thy	Fri Dec 04 12:21:15 2009 +0100
+++ b/LFex.thy	Fri Dec 04 14:11:03 2009 +0100
@@ -260,7 +260,7 @@
 apply - 
 apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_EQUIVs} 1 *})
 (*apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-apply(tactic {* all_inj_repabs_tac' @{context} rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})
 apply(tactic {* clean_tac @{context} 1 *})
 *)
 (*apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})*)