--- a/LFex.thy	Sun Dec 06 00:00:47 2009 +0100
+++ b/LFex.thy	Sun Dec 06 06:39:32 2009 +0100
@@ -260,7 +260,7 @@
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_equivps} 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})
-apply(fold perm_kind_def perm_ty_def perm_trm_def FV_ty_def[simplified id_simps] FV_kind_def[simplified id_simps] FV_trm_def[simplified id_simps])
+apply(fold perm_kind_def perm_ty_def perm_trm_def)
 apply(tactic {* clean_tac @{context} 1 *})
 (*
 Profiling: