--- a/QuotScript.thy	Fri Dec 04 11:06:43 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 11:33:58 2009 +0100
@@ -268,8 +268,8 @@
 
 lemma EQUALS_RSP:
   assumes q: "QUOTIENT R Abs Rep"
-  and     a: "R x1 x2" "R y1 y2"
-  shows "R x1 y1 = R x2 y2"
+  and     a: "R xa xb" "R ya yb"
+  shows "R xa ya = R xb yb"
 using QUOTIENT_SYM[OF q] QUOTIENT_TRANS[OF q] unfolding SYM_def TRANS_def
 using a by blast