--- a/Nominal/NewAlpha.thy	Fri May 14 10:28:42 2010 +0200
+++ b/Nominal/NewAlpha.thy	Fri May 14 15:37:23 2010 +0200
@@ -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
 *}