--- a/LFex.thy	Thu Dec 03 14:00:43 2009 +0100
+++ b/LFex.thy	Thu Dec 03 14:02:05 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}
@@ -264,16 +259,18 @@
 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_EQUIVs} 1 *})
+prefer 2
+apply(tactic {* clean_tac @{context} quot 1 *})
 (*
 Profiling:
 ML_prf {* fun ith i =  (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}
 ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *}
 ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *}
+ML_prf {* PolyML.profiling 1 *}
+ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *}
 *)
-apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-prefer 2
-apply(tactic {* clean_tac @{context} quot defs 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *})
 done
 
 (* Does not work:
@@ -303,7 +300,7 @@
 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *})
-apply(tactic {* clean_tac @{context} quot defs 1 *})
+apply(tactic {* clean_tac @{context} quot 1 *})
 done
 
 print_quotients