--- a/LamEx.thy	Wed Nov 25 15:43:12 2009 +0100
+++ b/LamEx.thy	Wed Nov 25 21:48:32 2009 +0100
@@ -179,7 +179,7 @@
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val consts = lookup_quot_consts defs *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
-ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *}
+ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs *}
 
 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
 apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
@@ -224,16 +224,12 @@
 apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *})
 done
 
-ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *}
-ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *}
 lemma alpha_induct: "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b);
      \<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
      \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam.
         \<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk>
     \<Longrightarrow> qxb qx qxa"
 apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *})
-apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *})
-apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
 done
 
 lemma var_inject: "(Var a = Var b) = (a = b)"