diff -r a08eaea622d1 -r cfda1ec86a9e Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Mon Apr 19 09:25:43 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Mon Apr 19 09:25:55 2010 +0200
@@ -7,6 +7,7 @@
 signature NOMINAL_LIBRARY =
 sig
   val mk_minus: term -> term
+  val mk_perm_ty: typ -> term -> term -> term
   val mk_perm: term -> term -> term
   val dest_perm: term -> term * term
 
@@ -21,12 +22,10 @@
 fun mk_minus p = 
  Const (@{const_name "uminus"}, @{typ "perm => perm"}) $ p
 
-fun mk_perm p trm =
-let
-  val ty = fastype_of trm
-in
+fun mk_perm_ty ty p trm =
   Const (@{const_name "permute"}, @{typ "perm"} --> ty --> ty) $ p $ trm
-end
+
+fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
 
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
   | dest_perm t = raise TERM ("dest_perm", [t])