diff -r fdccdc52c68a -r 02fd9de9d45e Quot/Examples/LFex.thy
--- a/Quot/Examples/LFex.thy	Tue Dec 08 23:32:54 2009 +0100
+++ b/Quot/Examples/LFex.thy	Wed Dec 09 00:03:18 2009 +0100
@@ -252,12 +252,10 @@
          ((x3 ::TY) = x4 \<longrightarrow> P2 x3 x4) \<and> 
          ((x5 :: TRM) = x6 \<longrightarrow> P3 x5 x6)"
 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} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1 *})
+apply(lifting akind_aty_atrm.induct)
+(* FIXME: with overloaded definitions *)
 apply(fold perm_kind_def perm_ty_def perm_trm_def)
-apply(tactic {* clean_tac @{context} 1 *})
+apply(cleaning)
 (*
 Profiling:
 ML_prf {* fun ith i =  (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *}
@@ -292,7 +290,7 @@
   \<And>trm1 trm2. \<lbrakk>R trm1; R trm2\<rbrakk> \<Longrightarrow> R (APP trm1 trm2);
   \<And>ty name trm. \<lbrakk>Q ty; R trm\<rbrakk> \<Longrightarrow> R (LAM ty name trm)\<rbrakk>
   \<Longrightarrow> P mkind \<and> Q mty \<and> R mtrm"
-apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} 1 *})
+apply(lifting kind_ty_trm.induct)
 done
 
 end