diff -r f8c8e2afcc18 -r 8e0bfb14f6bf Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Mon Apr 19 17:26:07 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Tue Apr 20 07:44:47 2010 +0200
@@ -9,6 +9,7 @@
   val mk_minus: term -> term
   val mk_plus: term -> term -> term
 
+  val perm_ty: typ -> typ 
   val mk_perm_ty: typ -> term -> term -> term
   val mk_perm: term -> term -> term
   val dest_perm: term -> term * term
@@ -27,8 +28,10 @@
 fun mk_plus p q =
  @{term "plus::perm => perm => perm"} $ p $ q
 
+fun perm_ty ty = @{typ perm} --> ty --> ty 
+
 fun mk_perm_ty ty p trm =
-  Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm
+  Const (@{const_name "permute"}, perm_ty ty) $ p $ trm
 
 fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm