--- a/Nominal/Nominal2_Abs.thy	Tue Apr 10 15:21:07 2012 +0100
+++ b/Nominal/Nominal2_Abs.thy	Tue Apr 10 15:22:16 2012 +0100
@@ -985,10 +985,10 @@
   by auto
 
 lemma [quot_preserve]:
-  assumes q1: "Quotient R1 abs1 rep1"
-  and     q2: "Quotient R2 abs2 rep2"
+  assumes q1: "Quotient3 R1 abs1 rep1"
+  and     q2: "Quotient3 R2 abs2 rep2"
   shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_pair rep1 rep2 ---> id) prod_fv = prod_fv"
-  by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+  by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
 
 lemma [mono]: 
   shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"