--- a/Quot/QuotSum.thy	Wed Feb 10 12:30:26 2010 +0100
+++ b/Quot/QuotSum.thy	Wed Feb 10 17:02:29 2010 +0100
@@ -69,7 +69,7 @@
   shows "(R2 ===> sum_rel R1 R2) Inr Inr"
   by simp
 
-lemma sum_Inl_prs[quot_respect]:
+lemma sum_Inl_prs[quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep1 ---> sum_map Abs1 Abs2) Inl = Inl"
@@ -77,7 +77,7 @@
   apply(simp add: Quotient_abs_rep[OF q1])
   done
 
-lemma sum_Inr_prs[quot_respect]:
+lemma sum_Inr_prs[quot_preserve]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   assumes q2: "Quotient R2 Abs2 Rep2"
   shows "(Rep2 ---> sum_map Abs1 Abs2) Inr = Inr"