diff -r b55098314f83 -r 6ad2f1c296a7 Nominal/Ex/LetRecB.thy
--- a/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:34:07 2011 +0100
+++ b/Nominal/Ex/LetRecB.thy	Tue Jun 28 14:49:48 2011 +0100
@@ -29,16 +29,16 @@
 
 
 lemma Abs_lst_fcb2:
-  fixes as bs :: "atom list"
+  fixes as bs :: "'a :: fs"
     and x y :: "'b :: fs"
     and c::"'c::fs"
-  assumes eq: "[bf as]lst. x = [bf bs]lst. y"
-  and fcb1: "(set (bf as)) \<sharp>* f as x c"
-  and fresh1: "set (bf as) \<sharp>* c"
-  and fresh2: "set (bf bs) \<sharp>* c"
+  assumes eq: "[ba as]lst. x = [ba bs]lst. y"
+  and fcb1: "(set (ba as)) \<sharp>* f as x c"
+  and fresh1: "set (ba as) \<sharp>* c"
+  and fresh2: "set (ba bs) \<sharp>* c"
   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"
   and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"
-  and props: "eqvt bf" "inj bf"
+  and props: "eqvt ba" "inj ba"
   shows "f as x c = f bs y c"
 proof -
   have "supp (as, x, c) supports (f as x c)"
@@ -52,20 +52,20 @@
   then have fin2: "finite (supp (f bs y c))"
     by (auto intro: supports_finite simp add: finite_supp)
   obtain q::"perm" where 
-    fr1: "(q \<bullet> (set (bf as))) \<sharp>* (x, c, f as x c, f bs y c)" and 
-    fr2: "supp q \<sharp>* ([bf as]lst. x)" and 
-    inc: "supp q \<subseteq> (set (bf as)) \<union> q \<bullet> (set (bf as))"
-    using at_set_avoiding3[where xs="set (bf as)" and c="(x, c, f as x c, f bs y c)" and x="[bf as]lst. x"]  
+    fr1: "(q \<bullet> (set (ba as))) \<sharp>* (x, c, f as x c, f bs y c)" and 
+    fr2: "supp q \<sharp>* ([ba as]lst. x)" and 
+    inc: "supp q \<subseteq> (set (ba as)) \<union> q \<bullet> (set (ba as))"
+    using at_set_avoiding3[where xs="set (ba as)" and c="(x, c, f as x c, f bs y c)" and x="[ba as]lst. x"]  
       fin1 fin2
     by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv)
-  have "[q \<bullet> (bf as)]lst. (q \<bullet> x) = q \<bullet> ([bf as]lst. x)" by simp
-  also have "\<dots> = [bf as]lst. x"
+  have "[q \<bullet> (ba as)]lst. (q \<bullet> x) = q \<bullet> ([ba as]lst. x)" by simp
+  also have "\<dots> = [ba as]lst. x"
     by (simp only: fr2 perm_supp_eq)
-  finally have "[q \<bullet> (bf as)]lst. (q \<bullet> x) = [bf bs]lst. y" using eq by simp
+  finally have "[q \<bullet> (ba as)]lst. (q \<bullet> x) = [ba bs]lst. y" using eq by simp
   then obtain r::perm where 
     qq1: "q \<bullet> x = r \<bullet> y" and 
-    qq2: "q \<bullet> (bf as) = r \<bullet> (bf bs)" and 
-    qq3: "supp r \<subseteq> (q \<bullet> (set (bf as))) \<union> set (bf bs)"
+    qq2: "q \<bullet> (ba as) = r \<bullet> (ba bs)" and 
+    qq3: "supp r \<subseteq> (q \<bullet> (set (ba as))) \<union> set (ba bs)"
     apply(drule_tac sym)
     apply(simp only: Abs_eq_iff2 alphas)
     apply(erule exE)
@@ -78,24 +78,24 @@
     apply(perm_simp)
     apply(simp)
     done
-  have "(set (bf as)) \<sharp>* f as x c" by (rule fcb1)
-  then have "q \<bullet> ((set (bf as)) \<sharp>* f as x c)"
+  have "(set (ba as)) \<sharp>* f as x c" by (rule fcb1)
+  then have "q \<bullet> ((set (ba as)) \<sharp>* f as x c)"
     by (simp add: permute_bool_def)
-  then have "set (q \<bullet> (bf as)) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c"
+  then have "set (q \<bullet> (ba as)) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c"
     apply(simp add: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm1)
     using inc fresh1 fr1
     apply(auto simp add: fresh_star_def fresh_Pair)
     done
-  then have "set (r \<bullet> (bf bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 qq4
+  then have "set (r \<bullet> (ba bs)) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 qq4
     by simp
-  then have "r \<bullet> ((set (bf bs)) \<sharp>* f bs y c)"
+  then have "r \<bullet> ((set (ba bs)) \<sharp>* f bs y c)"
     apply(simp add: fresh_star_eqvt set_eqvt)
     apply(subst (asm) perm2[symmetric])
     using qq3 fresh2 fr1
     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)
     done
-  then have fcb2: "(set (bf bs)) \<sharp>* f bs y c" by (simp add: permute_bool_def)
+  then have fcb2: "(set (ba bs)) \<sharp>* f bs y c" by (simp add: permute_bool_def)
   have "f as x c = q \<bullet> (f as x c)"
     apply(rule perm_supp_eq[symmetric])
     using inc fcb1 fr1 by (auto simp add: fresh_star_def)
@@ -144,7 +144,8 @@
   apply(simp)
   apply(simp add: inj_on_def)
   --"HERE"
-  apply (drule_tac c="()" in Abs_lst_fcb2)
+  thm Abs_lst_fcb Abs_lst_fcb2
+  apply (drule_tac c="()" and ba="bn" in Abs_lst_fcb2)
   prefer 8
   apply(assumption)
   apply (drule_tac c="()" in Abs_lst_fcb2)