--- a/LamEx.thy	Fri Nov 27 09:16:32 2009 +0100
+++ b/LamEx.thy	Fri Nov 27 10:04:49 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] rty [quot] trans2 rsp_thms defs *}
+ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms 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 *})