diff -r 040519ec99e9 -r b52e8651591f Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Mon Jan 13 15:42:10 2014 +0000
+++ b/Nominal/Nominal2_Abs.thy	Thu Mar 13 09:21:31 2014 +0000
@@ -479,14 +479,14 @@
   shows "(op= ===> op= ===> alpha_abs_set) Pair Pair"
   and   "(op= ===> op= ===> alpha_abs_res) Pair Pair"
   and   "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
-  unfolding fun_rel_def
+  unfolding rel_fun_def
   by (auto intro: alphas_abs_refl)
 
 lemma [quot_respect]:
   shows "(op= ===> alpha_abs_set ===> alpha_abs_set) permute permute"
   and   "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute"
   and   "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"
-  unfolding fun_rel_def
+  unfolding rel_fun_def
   by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
 
 lemma Abs_eq_iff:
@@ -1045,18 +1045,18 @@
 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"
+ "prod_alpha = rel_prod"
 
 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
+  shows "((R1 ===> op =) ===> (R2 ===> op =) ===> rel_prod R1 R2 ===> op =) prod_fv prod_fv"
+  unfolding rel_fun_def
+  unfolding rel_prod_def
   by auto
 
 lemma [quot_preserve]:
   assumes q1: "Quotient3 R1 abs1 rep1"
   and     q2: "Quotient3 R2 abs2 rep2"
-  shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_pair rep1 rep2 ---> id) prod_fv = prod_fv"
+  shows "((abs1 ---> id) ---> (abs2 ---> id) ---> map_prod rep1 rep2 ---> id) prod_fv = prod_fv"
   by (simp add: fun_eq_iff Quotient3_abs_rep[OF q1] Quotient3_abs_rep[OF q2])
 
 lemma [mono]: 
@@ -1067,7 +1067,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_def
+  unfolding rel_prod_def
   by (perm_simp) (rule refl)
 
 lemma [eqvt]: