--- a/LamEx.thy Fri Nov 27 07:16:16 2009 +0100
+++ b/LamEx.thy Fri Nov 27 08:15:23 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 absrep 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 *})