diff -r 2873b3230c44 -r 42c0d011a177 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Wed Jan 19 18:07:29 2011 +0100
+++ b/Nominal/Nominal2_Abs.thy	Wed Jan 19 18:56:28 2011 +0100
@@ -744,8 +744,7 @@
   and   "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> x = (c \<rightleftharpoons> d) \<bullet> y \<and> c \<sharp> y)"
 proof -
   { assume "a = b"
-    then have "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y)"
-      by (simp add: Abs1_eq)
+    then have "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
   }
   moreover
   { assume *: "a \<noteq> b" and **: "Abs_set {a} x = Abs_set {b} y"
@@ -769,8 +768,7 @@
     by blast
 next
   { assume "a = b"
-    then have "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y)"
-      by (simp add: Abs1_eq)
+    then have "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y)" by (simp add: Abs1_eq)
   }
   moreover
   { assume *: "a \<noteq> b" and **: "Abs_res {a} x = Abs_res {b} y"
@@ -794,8 +792,7 @@
     by blast
 next
   { assume "c = d"
-    then have "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y)"
-      by (simp add: Abs1_eq)
+    then have "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y)" by (simp add: Abs1_eq)
   }
   moreover
   { assume *: "c \<noteq> d" and **: "Abs_lst [c] x = Abs_lst [d] y"
@@ -819,6 +816,15 @@
     by blast
 qed
 
+lemma Abs1_eq_iff':
+  fixes x::"'a::fs"
+  assumes "sort_of a = sort_of b"
+  and     "sort_of c = sort_of d"
+  shows "Abs_set {a} x = Abs_set {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<rightleftharpoons> a) \<bullet> x = y \<and> b \<sharp> x)"
+  and   "Abs_res {a} x = Abs_res {b} y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<rightleftharpoons> a) \<bullet> x = y \<and> b \<sharp> x)"
+  and   "Abs_lst [c] x = Abs_lst [d] y \<longleftrightarrow> (c = d \<and> x = y) \<or> (c \<noteq> d \<and> (d \<rightleftharpoons> c) \<bullet> x = y \<and> d \<sharp> x)"
+using assms by (auto simp add: Abs1_eq_iff fresh_permute_left)
+
 
 subsection {* Renaming of bodies of abstractions *}