diff -r 217db3103f6a -r bb276771d85c Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Wed Dec 09 22:05:11 2009 +0100
+++ b/Quot/QuotScript.thy	Wed Dec 09 22:43:11 2009 +0100
@@ -510,7 +510,7 @@
 lemma rep_abs_rsp_left:
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
-  shows "R x1 (Rep (Abs x2))"
+  shows "R (Rep (Abs x1)) x2"
 using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])