--- a/LFex.thy	Mon Nov 30 15:40:22 2009 +0100
+++ b/LFex.thy	Tue Dec 01 12:16:45 2009 +0100
@@ -265,9 +265,6 @@
          ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
 using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11
 apply - 
-apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
-ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
-ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm akind_aty_atrm.induct})) (term_of qtm) *}
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2  1*})
@@ -461,7 +458,7 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2  1*})
 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2  1*})
-apply(tactic {* clean_tac @{context} quot defs aps 1 *})
+apply(tactic {* clean_tac @{context} quot defs 1 *})
 done
 
 (* Does not work:
@@ -488,14 +485,8 @@
   \<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 {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *})
-ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *}
-ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm kind_ty_trm.induct})) (term_of qtm) *}
 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-prefer 2
-apply(tactic {* clean_tac @{context} quot defs aps 1 *})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *})
@@ -587,6 +578,7 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
 apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* clean_tac @{context} quot defs 1 *})
 done
 
 print_quotients