--- a/QuotScript.thy	Thu Oct 22 13:45:48 2009 +0200
+++ b/QuotScript.thy	Thu Oct 22 15:02:01 2009 +0200
@@ -474,7 +474,7 @@
   using a by (metis COMBC_def Collect_def Collect_mem_eq)
 
 lemma RES_FORALL_RSP:
-  assumes a: "QUOTIENT R abs rep"
+  assumes a: "QUOTIENT R absf repf"
   shows "\<And>f g. (R ===> (op =)) f g ==>
         (Ball (Respects R) f = Ball (Respects R) g)"
   sorry