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