--- a/Nominal/Test_compat.thy	Tue Mar 09 09:54:58 2010 +0100
+++ b/Nominal/Test_compat.thy	Tue Mar 09 09:55:19 2010 +0100
@@ -20,6 +20,7 @@
   "bi (BP x t) = {atom x}"
 
 thm alpha_lam_raw_alpha_bp_raw.intros[no_vars]
+thm fv_lam_raw_fv_bp_raw.simps[no_vars]
 
 abbreviation "VAR \<equiv> VAR_raw"
 abbreviation "APP \<equiv> APP_raw"
@@ -28,6 +29,20 @@
 abbreviation "bi \<equiv> bi_raw"
 
 (* non-recursive case *)
+primrec
+    fv_lam :: "lam_raw \<Rightarrow> atom set"
+and fv_compat :: "bp_raw \<Rightarrow> atom set"
+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_compat bp) \<union> (fv_lam lam - bi bp)"
+| "fv_compat (BP name lam) = fv_lam lam"
+
+primrec
+    fv_bp :: "bp_raw \<Rightarrow> atom set"
+where
+  "fv_bp (BP name lam) = {atom name} \<union> fv_lam lam"
+
 
 inductive
   alpha_lam :: "lam_raw \<Rightarrow> lam_raw \<Rightarrow> bool" and
@@ -42,7 +57,6 @@
 | "alpha_lam t t' \<and> pi \<bullet> x = x' \<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))
                    (LET (BP y (VAR x)) (VAR y))"
 apply(rule alpha_lam_alpha_bp_compat_bp.intros)