diff -r 3e92714ce76a -r f8c8e2afcc18 Nominal/Rsp.thy
--- 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