--- a/Nominal/Test_compat1.thy	Tue Mar 09 09:55:19 2010 +0100
+++ b/Nominal/Test_compat1.thy	Tue Mar 09 11:06:57 2010 +0100
@@ -29,31 +29,42 @@
 
 (* non-recursive case *)
 
+fun
+    fv_lam
+and fv_bi
+and fv_bp
+where
+  "fv_lam (VAR name) = {atom name}"
+| "fv_lam (APP lam1 lam2) = fv_lam lam1 \<union> fv_lam lam2"
+| "fv_lam (LET bp lam) = (fv_bi bp) \<union> (fv_lam lam - bi bp)"
+| "fv_bi (BP name lam) = fv_lam lam"
+| "fv_bp (BP name lam) = {atom name} \<union> fv_lam lam"
+
 inductive
   alpha_lam :: "lam_raw \<Rightarrow> lam_raw \<Rightarrow> bool" and
   alpha_bp  :: "bp_raw \<Rightarrow> bp_raw \<Rightarrow> bool" and
-  compat_bp :: "bp_raw \<Rightarrow> perm \<Rightarrow> bp_raw \<Rightarrow> bool"
+  alpha_bi  :: "bp_raw \<Rightarrow> perm \<Rightarrow> bp_raw \<Rightarrow> bool"
 where
   "x = y \<Longrightarrow> alpha_lam (VAR x) (VAR y)"
 | "alpha_lam l1 s1 \<and> alpha_lam l2 s2 \<Longrightarrow> alpha_lam (APP l1 l2) (APP s1 s2)"
 | "\<exists>pi. (bi bp, lam) \<approx>gen alpha_lam fv_lam_raw pi (bi bp', lam') \<and> (pi \<bullet> (bi bp)) = bi bp' 
-   \<and> compat_bp bp pi bp' 
+   \<and> alpha_bi bp pi bp' 
    \<Longrightarrow> alpha_lam (LET bp lam) (LET bp' lam')"
 | "alpha_lam lam lam' \<and> name = name' \<Longrightarrow> alpha_bp (BP name lam) (BP name' lam')"
-| "alpha_lam t t' \<Longrightarrow> compat_bp (BP x t) pi (BP x' t')" 
+| "alpha_lam t t' \<Longrightarrow> alpha_bi (BP x t) pi (BP x' t')" 
 
 lemma test1:
   assumes "distinct [x, y]"
   shows "alpha_lam (LET (BP x (VAR x)) (VAR x))
                    (LET (BP y (VAR x)) (VAR y))"
-apply(rule alpha_lam_alpha_bp_compat_bp.intros)
+apply(rule alpha_lam_alpha_bp_alpha_bi.intros)
 apply(rule_tac x="(x \<leftrightarrow> y)" in exI)
 apply(simp add: alpha_gen fresh_star_def)
-apply(simp add: alpha_lam_alpha_bp_compat_bp.intros(1))
+apply(simp add: alpha_lam_alpha_bp_alpha_bi.intros(1))
 apply(rule conjI)
 defer
-apply(rule alpha_lam_alpha_bp_compat_bp.intros)
-apply(simp add: alpha_lam_alpha_bp_compat_bp.intros(1))
+apply(rule alpha_lam_alpha_bp_alpha_bi.intros)
+apply(simp add: alpha_lam_alpha_bp_alpha_bi.intros(1))
 apply(simp add: permute_set_eq atom_eqvt)
 done
 
@@ -71,7 +82,7 @@
 apply(erule alpha_lam.cases)
 apply(simp_all)
 apply(clarify)
-apply(erule compat_bp.cases)
+apply(erule alpha_bi.cases)
 apply(simp_all)
 apply(clarify)
 apply(erule alpha_lam.cases)
@@ -93,6 +104,8 @@
 | "Alpha_lam lam lam' \<and> name = name' \<Longrightarrow> Alpha_bp (BP name lam) (BP name' lam')"
 | "Alpha_lam (pi \<bullet> t) t' \<Longrightarrow> Compat_bp (BP x t) pi (BP x' t')"
 
+
+
 lemma Test1:
   assumes "distinct [x, y]"
   shows "Alpha_lam (LET (BP x (VAR x)) (VAR x))