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