--- a/Nominal/Nominal2_Abs.thy	Tue Jan 03 01:42:10 2012 +0000
+++ b/Nominal/Nominal2_Abs.thy	Tue Jan 03 11:43:27 2012 +0000
@@ -365,7 +365,7 @@
   then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
   from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast
   then have zb: "p \<bullet> as = p' \<bullet> as" 
-    apply(auto simp add: permute_set_eq)
+    apply(auto simp add: permute_set_def)
     apply(rule_tac x="xa" in exI)
     apply(simp)
     done
@@ -800,7 +800,7 @@
   moreover
   { assume *: "a \<noteq> b" and **: "Abs_set {a} x = Abs_set {b} y"
     have #: "a \<sharp> Abs_set {b} y" by (simp add: **[symmetric] Abs_fresh_iff)
-    have "Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_set {b} y)" by (simp add: permute_set_eq assms)
+    have "Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_set {b} y)" by (simp add: permute_set_def assms)
     also have "\<dots> = Abs_set {b} y"
       by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
     also have "\<dots> = Abs_set {a} x" using ** by simp
@@ -809,7 +809,7 @@
   moreover 
   { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"
     have "Abs_set {a} x = Abs_set {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp
-    also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_set {b} y" by (simp add: permute_set_eq assms)
+    also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_set {b} y" by (simp add: permute_set_def assms)
     also have "\<dots> = Abs_set {b} y"
       by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
     finally have "Abs_set {a} x = Abs_set {b} y" .
@@ -824,7 +824,7 @@
   moreover
   { assume *: "a \<noteq> b" and **: "Abs_res {a} x = Abs_res {b} y"
     have #: "a \<sharp> Abs_res {b} y" by (simp add: **[symmetric] Abs_fresh_iff)
-    have "Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_res {b} y)" by (simp add: permute_set_eq assms)
+    have "Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y) = (a \<rightleftharpoons> b) \<bullet> (Abs_res {b} y)" by (simp add: permute_set_def assms)
     also have "\<dots> = Abs_res {b} y"
       by (rule swap_fresh_fresh) (simp add: #, simp add: Abs_fresh_iff)
     also have "\<dots> = Abs_res {a} x" using ** by simp
@@ -833,7 +833,7 @@
   moreover 
   { assume *: "a \<noteq> b" and **: "x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y"
     have "Abs_res {a} x = Abs_res {a} ((a \<rightleftharpoons> b) \<bullet> y)" using ** by simp
-    also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_res {b} y" by (simp add: permute_set_eq assms)
+    also have "\<dots> = (a \<rightleftharpoons> b) \<bullet> Abs_res {b} y" by (simp add: permute_set_def assms)
     also have "\<dots> = Abs_res {b} y"
       by (rule swap_fresh_fresh) (simp add: Abs_fresh_iff **, simp add: Abs_fresh_iff)
     finally have "Abs_res {a} x = Abs_res {b} y" .