diff -r 1b7c034c9e9e -r 0440bc1a2438 Nominal/Ex/Pi.thy
--- a/Nominal/Ex/Pi.thy	Mon Jun 18 14:50:02 2012 +0100
+++ b/Nominal/Ex/Pi.thy	Thu Jul 12 10:11:32 2012 +0100
@@ -103,7 +103,7 @@
   assume "a \<noteq> z"
   thus ?thesis
     using assms
-    by(simp add: piMix_eq_iff Abs1_eq_iff fresh_permute_left)
+    by (simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
 qed
 
 lemma alphaInput_mix:
@@ -123,7 +123,7 @@
   assume "b \<noteq> z"
   thus ?thesis
     using assms
-    by(simp add: piMix_eq_iff Abs1_eq_iff fresh_permute_left)
+    by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
 qed
 
 lemma alphaRep_mix:
@@ -143,7 +143,7 @@
   assume "b \<noteq> z"
   thus ?thesis
     using assms
-    by(simp add: piMix_eq_iff Abs1_eq_iff fresh_permute_left)
+    by(simp add: flip_def piMix_eq_iff Abs1_eq_iff fresh_permute_left)
 qed
 
 subsection {* Capture-Avoiding Substitution of Names *}
@@ -393,7 +393,7 @@
   apply(simp add: finite_supp)
   apply(simp)
   apply(simp add: eqvt_at_def)
-  apply(drule_tac x="(atom b \<rightleftharpoons> atom ba)" in spec)
+  apply(drule_tac x="(b \<leftrightarrow> ba)" in spec)
   apply(simp)
   done