--- a/Nominal/Abs.thy	Sat Sep 18 05:13:42 2010 +0800
+++ b/Nominal/Abs.thy	Sat Sep 18 06:09:43 2010 +0800
@@ -552,7 +552,7 @@
   assumes q1: "Quotient R1 abs1 rep1"
   and     q2: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> id) ---> (abs2 ---> id) ---> prod_fun rep1 rep2 ---> id) prod_fv = prod_fv"
-  by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
+  by (simp add: fun_eq_iff Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
 lemma [mono]: 
   shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"