--- a/Nominal/Equivp.thy	Mon Apr 19 16:55:57 2010 +0200
+++ b/Nominal/Equivp.thy	Mon Apr 19 17:26:07 2010 +0200
@@ -346,7 +346,7 @@
   val typ = domain_type (fastype_of fnctn);
   val arg = the (AList.lookup (op=) frees typ);
 in
-  ([HOLogic.mk_eq ((perm_arg (fnctn $ arg) $ pi $ (fnctn $ arg)), (fnctn $ (perm_arg arg $ pi $ arg)))], ctxt)
+  ([HOLogic.mk_eq (mk_perm pi (fnctn $ arg), fnctn $ (mk_perm pi arg))], ctxt)
 end
 *}
 

--- a/Nominal/Rsp.thy	Mon Apr 19 16:55:57 2010 +0200
+++ b/Nominal/Rsp.thy	Mon Apr 19 17:26:07 2010 +0200
@@ -87,14 +87,6 @@
   ))
 *}
 
-ML {*
-fun perm_arg arg =
-let
-  val ty = fastype_of arg
-in
-  Const (@{const_name permute}, @{typ perm} --> ty --> ty)
-end
-*}
 
 lemma exi: "\<exists>(pi :: perm). P pi \<Longrightarrow> (\<And>(p :: perm). P p \<Longrightarrow> Q (pi \<bullet> p)) \<Longrightarrow> \<exists>pi. Q pi"
 apply (erule exE)
@@ -123,7 +115,7 @@
   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
+  val perm_args = map (fn x => mk_perm pi x) args
 in
   (HOLogic.mk_imp (list_comb (alpha, args), list_comb (alpha, perm_args)), indnames @ names)
 end