--- a/Nominal/Rsp.thy	Mon Mar 15 10:36:09 2010 +0100
+++ b/Nominal/Rsp.thy	Mon Mar 15 11:50:12 2010 +0100
@@ -135,6 +135,16 @@
 *}
 
 ML {*
+fun perm_arg arg =
+let
+  val ty = fastype_of arg
+in
+  Const (@{const_name permute}, @{typ perm} --> ty --> ty)
+end
+*}
+
+
+ML {*
 fun build_eqvts bind funs tac ctxt =
 let
   val pi = Free ("p", @{typ perm});
@@ -142,7 +152,6 @@
   val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames types);
   val args = map Free (indnames ~~ types);
   val perm_at = @{term "permute :: perm \<Rightarrow> atom set \<Rightarrow> atom set"}
-  fun perm_arg arg = Const (@{const_name permute}, @{typ perm} --> fastype_of arg --> fastype_of arg)
   fun eqvtc (fnctn, arg) =
     HOLogic.mk_eq ((perm_at $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))
   val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc (funs ~~ args)))
@@ -181,19 +190,26 @@
 *}
 
 ML {*
-fun build_alpha_eqvts funs perms tac ctxt =
+fun build_alpha_eqvt alpha names =
 let
   val pi = Free ("p", @{typ perm});
-  val types = map (domain_type o fastype_of) funs;
-  val indnames = Name.variant_list ["p"] (Datatype_Prop.make_tnames (map body_type types));
-  val indnames2 = Name.variant_list ("p" :: indnames) (Datatype_Prop.make_tnames (map body_type types));
-  val args = map Free (indnames ~~ types);
-  val args2 = map Free (indnames2 ~~ types);
-  fun eqvtc ((alpha, perm), (arg, arg2)) =
-    HOLogic.mk_imp (alpha $ arg $ arg2,
-      (alpha $ (perm $ pi $ arg) $ (perm $ pi $ arg2)))
-  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map eqvtc ((funs ~~ perms) ~~ (args ~~ args2))))
-  val thm = Goal.prove ctxt ("p" :: indnames @ indnames2) [] gl tac
+  val (tys, _) = strip_type (fastype_of alpha)
+  val indnames = Name.variant_list names (Datatype_Prop.make_tnames (map body_type tys));
+  val args = map Free (indnames ~~ tys);
+  val perm_args = map (fn x => perm_arg x $ pi $ x) args
+in
+  (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names)
+end
+*}
+
+ML {* fold_map build_alpha_eqvt *}
+
+ML {*
+fun build_alpha_eqvts funs tac ctxt =
+let
+  val (gls, names) = fold_map build_alpha_eqvt funs ["p"]
+  val gl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj gls)
+  val thm = Goal.prove ctxt names [] gl tac
 in
   map (fn x => mp OF [x]) (HOLogic.conj_elims thm)
 end