--- a/Nominal/Abs.thy	Thu May 13 15:12:05 2010 +0100
+++ b/Nominal/Abs.thy	Thu May 13 15:12:34 2010 +0100
@@ -843,11 +843,15 @@
 lemma [mono]: "A <= B \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D"
   by auto
 
-lemma [eqvt]: "(p \<bullet> prod_rel A B x y) = prod_rel (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
-  by (simp, perm_simp) (rule refl)
+lemma [eqvt]: 
+  shows "p \<bullet> prod_rel A B x y = prod_rel (p \<bullet> A) (p \<bullet> B) (p \<bullet> x) (p \<bullet> y)"
+  unfolding prod_rel.simps
+  by (perm_simp) (rule refl)
 
-lemma [eqvt]: "(p \<bullet> prod_fv A B (x, y)) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
-  by (simp, perm_simp) (rule refl)
+lemma [eqvt]: 
+  shows "p \<bullet> prod_fv A B (x, y) = prod_fv (p \<bullet> A) (p \<bullet> B) (p \<bullet> x, p \<bullet> y)"
+  unfolding prod_fv.simps
+  by (perm_simp) (rule refl)
 
 end