--- a/Nominal/Abs.thy	Sat Sep 04 06:10:04 2010 +0800
+++ b/Nominal/Abs.thy	Sat Sep 04 06:23:31 2010 +0800
@@ -461,7 +461,7 @@
   and   "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
   and   "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
   by (rule_tac [!] fresh_fun_eqvt_app)
-     (simp_all add: eqvts_raw)
+     (simp_all only: eqvts_raw)
 
 lemma supp_abs_subset1:
   assumes a: "finite (supp x)"
@@ -523,6 +523,15 @@
   unfolding supp_abs
   by auto
 
+lemma Abs_eq_iff:
+  shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
+  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
+  and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
+  by (lifting alphas_abs)
+
+
+section {* Infrastructure for building tuples of relations and functions *}
+
 fun
   prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
 where
@@ -560,16 +569,5 @@
   by (perm_simp) (rule refl)
 
 
-(* Below seems to be not needed *)
-
-(*
-lemma Abs_eq_iff:
-  shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
-  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
-  and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
-  by (lifting alphas_abs)
-*)
-
-
 end