--- a/LFex.thy	Thu Dec 03 13:45:52 2009 +0100
+++ b/LFex.thy	Thu Dec 03 13:56:59 2009 +0100
@@ -216,11 +216,6 @@
 thm akind_aty_atrm.induct
 thm kind_ty_trm.induct
 
-ML {* val defs =
-  @{thms TYP_def KPI_def TCONST_def TAPP_def TPI_def VAR_def CONS_def APP_def LAM_def
-    FV_kind_def FV_ty_def FV_trm_def perm_kind_def perm_ty_def perm_trm_def}
-*}
-
 ML {*
   val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM}
   val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs}
@@ -266,7 +261,6 @@
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
 prefer 2
-apply(tactic {* simp_tac ((Simplifier.context @{context} empty_ss) addsimps @{thms perm_kind_def perm_ty_def perm_trm_def}) 1 *})
 apply(tactic {* clean_tac @{context} quot 1 *})
 (*
 Profiling: