LamEx.thy
changeset 416 3f3927f793d4
parent 389 d67240113f68
child 417 cb81b40137c2
--- 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 *})