diff -r 84a13d1e2511 -r 0c9ef14e9ba4 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Tue Apr 27 22:21:16 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Tue Apr 27 22:45:50 2010 +0200
@@ -34,11 +34,9 @@
 fun mk_plus p q =
  @{term "plus::perm => perm => perm"} $ p $ q
 
-fun perm_ty ty = @{typ perm} --> ty --> ty 
-
+fun perm_ty ty = @{typ "perm"} --> ty --> ty 
 fun mk_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
 
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
@@ -47,7 +45,8 @@
 
 fun mk_sort_of t = @{term "sort_of"} $ t;
 
-fun mk_atom_ty T t = Const (@{const_name atom}, T --> @{typ atom}) $ t;
+fun atom_ty ty = ty --> @{typ "atom"}
+fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t;
 fun mk_atom t = mk_atom_ty (fastype_of t) t;
 
 fun mk_equiv r = r RS @{thm eq_reflection};