diff -r 77b86f1fc936 -r 416c9c5a1126 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Wed Mar 17 08:39:46 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 17 09:17:55 2010 +0100
@@ -139,9 +139,42 @@
       val c = HOLogic.pair_const ty1 ty2
     in c $ fst $ snd
     end;
+*}
 
+(* Given [fv1, fv2, fv3] creates %(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;
 *}
 
+ML {* @{term "\<lambda>(x, y, z). \<lambda>(x', y', z'). R x x' \<and> R2 y y' \<and> R3 z z'"} *}
+
+(* Given [R1, R2, R3] creates %(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 = mk_conjl 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 {* cterm_of @{theory} (mk_compound_alpha [@{term "R :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}, @{term "R2 :: 'b \<Rightarrow> 'b \<Rightarrow> bool"}, @{term "R3 :: 'b \<Rightarrow> 'b \<Rightarrow> bool"}]) *}
+
 ML {* fun add_perm (p1, p2) = Const(@{const_name plus}, @{typ "perm \<Rightarrow> perm \<Rightarrow> perm"}) $ p1 $ p2 *}
 
 ML {*
@@ -328,7 +361,9 @@
         let
           val rel_in_simp_binds = filter (fn ((NONE, i, _), _) => i = arg_no | _ => false) bind_pis;
           val rel_in_comp_binds = filter (fn ((SOME _, i, _), _) => i = arg_no | _ => false) bind_pis;
-          val rel_has_binds = filter (fn ((_, _, j), _) => j = arg_no | _ => false) bind_pis;
+          val rel_has_binds = filter (fn ((NONE, _, j), _) => j = arg_no
+                                       | ((SOME (_, false), _, j), _) => j = arg_no
+                                       | _ => false) bind_pis;
         in
           case (rel_in_simp_binds, rel_in_comp_binds, rel_has_binds) of
             ([], [], []) =>
@@ -340,14 +375,27 @@
             if is_rec then
               let
                 val (rbinds, rpis) = split_list rel_in_comp_binds
+                val bound_in_nos = map (fn (_, _, i) => i) rbinds
+                val bound_in_ty_nos = map (fn i => body_index (nth dts i)) bound_in_nos;
+                val bound_args = arg :: map (nth args) bound_in_nos;
+                val bound_args2 = arg2 :: map (nth args2) bound_in_nos;
+                fun bound_in args (_, _, i) = nth args i;
                 val lhs_binds = fv_binds args rbinds
-                val lhs = mk_pair (lhs_binds, arg);
+                val lhs_arg = foldr1 HOLogic.mk_prod bound_args
+                val lhs = mk_pair (lhs_binds, lhs_arg);
                 val rhs_binds = fv_binds args2 rbinds;
-                val rhs = mk_pair (rhs_binds, arg2);
-                val alpha = nth alpha_frees (body_index dt);
-                val fv = nth fv_frees (body_index dt);
+                val rhs_arg = foldr1 HOLogic.mk_prod bound_args2;
+                val rhs = mk_pair (rhs_binds, rhs_arg);
+                val _ = tracing (PolyML.makestring bound_in_ty_nos);
+                val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos);
+                val _ = tracing (PolyML.makestring fvs);
+                val fv = mk_compound_fv fvs;
+                val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos);
+                val _ = tracing (PolyML.makestring alphas);
+                val alpha = mk_compound_alpha alphas;
                 val pi = foldr1 add_perm (distinct (op =) rpis);
                 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs;
+                val _ = tracing (PolyML.makestring alpha_gen_pre);
                 val alpha_gen = Syntax.check_term lthy alpha_gen_pre
               in
                 alpha_gen