--- a/Nominal/Ex/SingleLetFoo.thy	Fri May 14 15:02:25 2010 +0100
+++ b/Nominal/Ex/SingleLetFoo.thy	Fri May 14 15:21:05 2010 +0100
@@ -14,6 +14,7 @@
 | Let a::"assg" t::"trm"  bind_set "bn a" in t
 | Foo1 a1::"assg" a2::"assg" t::"trm" bind_set "bn a1" "bn a2" in t
 | Foo2 x::name a::"assg" t::"trm" bind_set x "bn a" in t
+
 and assg =
   As "name" "trm"
 binder
@@ -25,6 +26,7 @@
 thm trm_assg.eq_iff
 thm trm_assg.supp
 thm trm_assg.perm
+thm trm_assg.fv[simplified trm_assg.supp(1-2),no_vars]
 
 thm permute_trm_raw_permute_assg_raw.simps
 thm fv_trm_raw.simps fv_assg_raw.simps fv_bn_raw.simps[no_vars]

--- a/Nominal/NewAlpha.thy	Fri May 14 15:02:25 2010 +0100
+++ b/Nominal/NewAlpha.thy	Fri May 14 15:21:05 2010 +0100
@@ -2,39 +2,6 @@
 imports "NewFv"
 begin
 
-(* Given [fv1, fv2, fv3]
-   produces %(x, y, z). fv1 x u fv2 y u fv3 z *)
-ML {*
-fun mk_compound_fv fvs =
-let
-  val nos = (length fvs - 1) downto 0;
-  val fvs_applied = map (fn (fv, no) => fv $ Bound no) (fvs ~~ nos);
-  val fvs_union = mk_union fvs_applied;
-  val (tyh :: tys) = rev (map (domain_type o fastype_of) fvs);
-  fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))
-in
-  fold fold_fun tys (Abs ("", tyh, fvs_union))
-end;
-*}
-
-(* Given [R1, R2, R3]
-   produces %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *)
-ML {*
-fun mk_compound_alpha Rs =
-let
-  val nos = (length Rs - 1) downto 0;
-  val nos2 = (2 * length Rs - 1) downto length Rs;
-  val Rs_applied = map (fn (R, (no2, no)) => R $ Bound no2 $ Bound no)
-    (Rs ~~ (nos2 ~~ nos));
-  val Rs_conj = foldr1 HOLogic.mk_conj Rs_applied;
-  val (tyh :: tys) = rev (map (domain_type o fastype_of) Rs);
-  fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))
-  val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj))
-in
-  fold fold_fun tys (Abs ("", tyh, abs_rhs))
-end;
-*}
-
 ML {*
 fun mk_binop2 ctxt s (l, r) =
   Syntax.check_term ctxt (Const (s, dummyT) $ l $ r)
@@ -85,11 +52,12 @@
   val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ (Bound 0) $ rhs
   val alpha_gen_ex = HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, alpha_gen_pre)
   val t = Syntax.check_term lthy alpha_gen_ex
+  fun alpha_bn_bind (SOME bn, i) =
+      if member (op =) bodys i then NONE
+      else SOME ((the (AList.lookup (op=) bn_alphabn bn)) $ nth args i $ nth args2 i)
+    | alpha_bn_bind (NONE, _) = NONE
 in
-  case binds of
-    [(SOME bn, i)] => if member (op =) bodys i then [t]
-      else [t, ((the (AList.lookup (op=) bn_alphabn bn)) $ nth args i $ nth args2 i)]
-    | _ => [t]
+  t :: (map_filter alpha_bn_bind binds)
 end
 *}
 

--- a/Nominal/NewFv.thy	Fri May 14 15:02:25 2010 +0100
+++ b/Nominal/NewFv.thy	Fri May 14 15:21:05 2010 +0100
@@ -136,15 +136,13 @@
   fun bound_var (SOME bn, i) = set (bn $ nth args i)
     | bound_var (NONE, i) = fv_body thy dts args fv_frees false i
   val bound_vars = mk_union (map bound_var binds);
-  val non_rec_vars =
-    case binds of
-      [(SOME bn, i)] =>
-        if member (op =) bodys i
-        then noatoms
-        else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
-    | _ => noatoms
+  fun non_rec_var (SOME bn, i) =
+      if member (op =) bodys i
+      then noatoms
+      else ((the (AList.lookup (op=) bn_fvbn bn)) $ nth args i)
+    | non_rec_var (NONE, _) = noatoms
 in
-  mk_union [mk_diff fv_bodys bound_vars, non_rec_vars]
+  mk_union ((mk_diff fv_bodys bound_vars) :: (map non_rec_var binds))
 end
 *}
 

--- a/Nominal/Unused.thy	Fri May 14 15:02:25 2010 +0100
+++ b/Nominal/Unused.thy	Fri May 14 15:21:05 2010 +0100
@@ -41,3 +41,35 @@
 end
 *}
 
+(* Given [fv1, fv2, fv3]
+   produces %(x, y, z). fv1 x u fv2 y u fv3 z *)
+ML {*
+fun mk_compound_fv fvs =
+let
+  val nos = (length fvs - 1) downto 0;
+  val fvs_applied = map (fn (fv, no) => fv $ Bound no) (fvs ~~ nos);
+  val fvs_union = mk_union fvs_applied;
+  val (tyh :: tys) = rev (map (domain_type o fastype_of) fvs);
+  fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))
+in
+  fold fold_fun tys (Abs ("", tyh, fvs_union))
+end;
+*}
+
+(* Given [R1, R2, R3]
+   produces %(x,x'). %(y,y'). %(z,z'). R x x' \<and> R y y' \<and> R z z' *)
+ML {*
+fun mk_compound_alpha Rs =
+let
+  val nos = (length Rs - 1) downto 0;
+  val nos2 = (2 * length Rs - 1) downto length Rs;
+  val Rs_applied = map (fn (R, (no2, no)) => R $ Bound no2 $ Bound no)
+    (Rs ~~ (nos2 ~~ nos));
+  val Rs_conj = foldr1 HOLogic.mk_conj Rs_applied;
+  val (tyh :: tys) = rev (map (domain_type o fastype_of) Rs);
+  fun fold_fun ty t = HOLogic.mk_split (Abs ("", ty, t))
+  val abs_rhs = fold fold_fun tys (Abs ("", tyh, Rs_conj))
+in
+  fold fold_fun tys (Abs ("", tyh, abs_rhs))
+end;
+*}