diff -r 1b7c034c9e9e -r 0440bc1a2438 Nominal/Nominal2_FCB.thy
--- a/Nominal/Nominal2_FCB.thy	Mon Jun 18 14:50:02 2012 +0100
+++ b/Nominal/Nominal2_FCB.thy	Thu Jul 12 10:11:32 2012 +0100
@@ -22,26 +22,25 @@
 
 
 lemma Abs_lst1_fcb:
-  fixes x y :: "'a :: at_base"
+  fixes x y :: "'a :: at"
     and S T :: "'b :: fs"
-  assumes e: "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)"
-  and f1: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (atom y \<rightleftharpoons> atom x) \<bullet> T\<rbrakk> \<Longrightarrow> atom x \<sharp> f x T"
-  and f2: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (atom y \<rightleftharpoons> atom x) \<bullet> T\<rbrakk> \<Longrightarrow> atom y \<sharp> f x T"
-  and p: "\<lbrakk>S = (atom x \<rightleftharpoons> atom y) \<bullet> T; x \<noteq> y; atom y \<sharp> T; atom x \<sharp> S\<rbrakk> 
-    \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S"
-  and s: "sort_of (atom x) = sort_of (atom y)"
+  assumes e: "[[atom x]]lst. T = [[atom y]]lst. S"
+  and f1: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (y \<leftrightarrow> x) \<bullet> T\<rbrakk> \<Longrightarrow> atom x \<sharp> f x T"
+  and f2: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (y \<leftrightarrow> x) \<bullet> T\<rbrakk> \<Longrightarrow> atom y \<sharp> f x T"
+  and p: "\<lbrakk>S = (x \<leftrightarrow> y) \<bullet> T; x \<noteq> y; atom y \<sharp> T; atom x \<sharp> S\<rbrakk> 
+    \<Longrightarrow> (x \<leftrightarrow> y) \<bullet> (f x T) = f y S"
   shows "f x T = f y S"
   using e
   apply(case_tac "atom x \<sharp> S")
-  apply(simp add: Abs1_eq_iff'[OF s s])
+  apply(simp add: Abs1_eq_iff')
   apply(elim conjE disjE)
   apply(simp)
   apply(rule trans)
-  apply(rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric])
+  apply(rule_tac p="(x \<leftrightarrow> y)" in supp_perm_eq[symmetric])
   apply(rule fresh_star_supp_conv)
-  apply(simp add: supp_swap fresh_star_def s f1 f2)
-  apply(simp add: swap_commute p)
-  apply(simp add: Abs1_eq_iff[OF s s])
+  apply(simp add: flip_def supp_swap fresh_star_def f1 f2)
+  apply(simp add: flip_commute p)
+  apply(simp add: Abs1_eq_iff)
   done
 
 lemma Abs_lst_fcb:
@@ -383,7 +382,7 @@
   fixes a b :: "atom"
     and x y :: "'b :: fs"
     and c::"'c :: fs"
-  assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)"
+  assumes e: "[[a]]lst. x = [[b]]lst. y"
   and fcb1: "a \<sharp> f a x c"
   and fresh: "{a, b} \<sharp>* c"
   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c"
@@ -400,7 +399,7 @@
   fixes a b :: "'a::at"
     and x y :: "'b :: fs"
     and c::"'c :: fs"
-  assumes e: "(Abs_lst [atom a] x) = (Abs_lst [atom b] y)"
+  assumes e: "[[atom a]]lst. x = [[atom b]]lst. y"
   and fcb1: "atom a \<sharp> f a x c"
   and fresh: "{atom a, atom b} \<sharp>* c"
   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c"