diff -r 91c374abde06 -r fac6069d8e80 LamEx.thy
--- a/LamEx.thy	Thu Dec 03 15:03:31 2009 +0100
+++ b/LamEx.thy	Fri Dec 04 08:18:38 2009 +0100
@@ -128,7 +128,7 @@
 unfolding fresh_def supp_def
 sorry
 
-lemma perm_rsp[quot_rsp]:
+lemma perm_rsp[quotient_rsp]:
   "(op = ===> alpha ===> alpha) op \<bullet> op \<bullet>"
   apply(auto)
   (* this is propably true if some type conditions are imposed ;o) *)
@@ -140,14 +140,14 @@
   (* this is probably only true if some type conditions are imposed *)
   sorry
 
-lemma rVar_rsp[quot_rsp]:
+lemma rVar_rsp[quotient_rsp]:
   "(op = ===> alpha) rVar rVar"
 by (auto intro:a1)
 
-lemma rApp_rsp[quot_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
+lemma rApp_rsp[quotient_rsp]: "(alpha ===> alpha ===> alpha) rApp rApp"
 by (auto intro:a2)
 
-lemma rLam_rsp[quot_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
+lemma rLam_rsp[quotient_rsp]: "(op = ===> alpha ===> alpha) rLam rLam"
   apply(auto)
   apply(rule a3)
   apply(rule_tac t="[(x,x)]\<bullet>y" and s="y" in subst)
@@ -160,7 +160,7 @@
   apply(simp add: abs_fresh)
   done
 
-lemma rfv_rsp[quot_rsp]: "(alpha ===> op =) rfv rfv"
+lemma rfv_rsp[quotient_rsp]: "(alpha ===> op =) rfv rfv"
   sorry
 
 lemma rvar_inject: "rVar a \<approx> rVar b = (a = b)"
@@ -174,7 +174,7 @@
 
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 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] [quot] *}
+ML {* fun lift_tac_lam lthy t = lift_tac lthy t [rel_eqv] *}
 
 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 *})