--- a/Nominal/Abs.thy	Wed May 26 15:37:56 2010 +0200
+++ b/Nominal/Abs.thy	Thu May 27 18:37:52 2010 +0200
@@ -847,7 +847,8 @@
   by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
 
 lemma [mono]: 
-  shows "A <= B \<Longrightarrow> C <= D ==> prod_rel A C <= prod_rel B D"
+  shows "A <= B \<Longrightarrow> C <= D ==> prod_alpha A C <= prod_alpha B D"
+  unfolding prod_alpha_def
   by auto
 
 lemma [eqvt]: 
@@ -861,5 +862,6 @@
   unfolding prod_fv.simps
   by (perm_simp) (rule refl)
 
+
 end