diff -r e0b4bca46c6a -r 672e14609e6e Quotients.thy
--- a/Quotients.thy	Thu Aug 20 10:31:44 2009 +0200
+++ b/Quotients.thy	Thu Aug 20 14:44:29 2009 +0200
@@ -138,7 +138,7 @@
 lemma QUOTIENT_PROD:
   assumes a: "QUOTIENT E1 Abs1 Rep1"
   and     b: "QUOTIENT E2 Abs2 Rep2"
-  shows "QUOTIENT (PROD_REL E1 e2) (prod_map Abs1 Abs2) (prod_map Rep1 rep2)"
+  shows "QUOTIENT (PROD_REL E1 E2) (prod_map Abs1 Abs2) (prod_map Rep1 Rep2)"
 using a b unfolding QUOTIENT_def
 oops