--- a/Nominal/Abs.thy	Sun May 23 02:15:24 2010 +0100
+++ b/Nominal/Abs.thy	Mon May 24 20:02:37 2010 +0100
@@ -830,8 +830,14 @@
 where
   "prod_fv fvx fvy (x, y) = (fvx x \<union> fvy y)"
 
+definition 
+  prod_alpha :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool)"
+where
+ "prod_alpha = prod_rel"
+
+
 lemma [quot_respect]:
-  "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
+  shows "((R1 ===> op =) ===> (R2 ===> op =) ===> prod_rel R1 R2 ===> op =) prod_fv prod_fv"
   by auto
 
 lemma [quot_preserve]:
@@ -840,11 +846,13 @@
   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])
 
-lemma [mono]: "A <= B \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D"
+lemma [mono]: 
+  shows "A <= B \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D"
   by auto
 
 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)"
+  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
   by (perm_simp) (rule refl)