--- a/Nominal/Abs.thy	Wed Nov 10 13:40:46 2010 +0000
+++ b/Nominal/Abs.thy	Wed Nov 10 13:46:21 2010 +0000
@@ -546,6 +546,8 @@
 
 lemma [quot_respect]:
   shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
+  unfolding fun_rel_def
+  unfolding prod_rel_def
   by auto
 
 lemma [quot_preserve]:
@@ -562,7 +564,7 @@
 lemma [eqvt]: 
   shows "p \<bullet> prod_alpha A B x y = prod_alpha (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
   unfolding prod_alpha_def
-  unfolding prod_rel.simps
+  unfolding prod_rel_def
   by (perm_simp) (rule refl)
 
 lemma [eqvt]: