--- a/Quot/Examples/LFex.thy	Tue Dec 08 16:36:01 2009 +0100
+++ b/Quot/Examples/LFex.thy	Tue Dec 08 17:30:00 2009 +0100
@@ -183,35 +183,35 @@
 end
 
 (* TODO/FIXME: Think whether these RSP theorems are true. *)
-lemma kpi_rsp[quotient_rsp]: 
+lemma kpi_rsp[quot_respect]: 
   "(aty ===> op = ===> akind ===> akind) KPi KPi" sorry
-lemma tconst_rsp[quotient_rsp]: 
+lemma tconst_rsp[quot_respect]: 
   "(op = ===> aty) TConst TConst" sorry
-lemma tapp_rsp[quotient_rsp]: 
+lemma tapp_rsp[quot_respect]: 
   "(aty ===> atrm ===> aty) TApp TApp" sorry
-lemma tpi_rsp[quotient_rsp]: 
+lemma tpi_rsp[quot_respect]: 
   "(aty ===> op = ===> aty ===> aty) TPi TPi" sorry
-lemma var_rsp[quotient_rsp]: 
+lemma var_rsp[quot_respect]: 
   "(op = ===> atrm) Var Var" sorry
-lemma app_rsp[quotient_rsp]: 
+lemma app_rsp[quot_respect]: 
   "(atrm ===> atrm ===> atrm) App App" sorry
-lemma const_rsp[quotient_rsp]: 
+lemma const_rsp[quot_respect]: 
   "(op = ===> atrm) Const Const" sorry
-lemma lam_rsp[quotient_rsp]: 
+lemma lam_rsp[quot_respect]: 
   "(aty ===> op = ===> atrm ===> atrm) Lam Lam" sorry
 
-lemma perm_kind_rsp[quotient_rsp]: 
+lemma perm_kind_rsp[quot_respect]: 
   "(op = ===> akind ===> akind) op \<bullet> op \<bullet>" sorry
-lemma perm_ty_rsp[quotient_rsp]: 
+lemma perm_ty_rsp[quot_respect]: 
   "(op = ===> aty ===> aty) op \<bullet> op \<bullet>" sorry
-lemma perm_trm_rsp[quotient_rsp]: 
+lemma perm_trm_rsp[quot_respect]: 
   "(op = ===> atrm ===> atrm) op \<bullet> op \<bullet>" sorry
 
-lemma fv_ty_rsp[quotient_rsp]: 
+lemma fv_ty_rsp[quot_respect]: 
   "(aty ===> op =) fv_ty fv_ty" sorry
-lemma fv_kind_rsp[quotient_rsp]: 
+lemma fv_kind_rsp[quot_respect]: 
   "(akind ===> op =) fv_kind fv_kind" sorry
-lemma fv_trm_rsp[quotient_rsp]: 
+lemma fv_trm_rsp[quot_respect]: 
   "(atrm ===> op =) fv_trm fv_trm" sorry