diff -r 774d631726ad -r 84a13d1e2511 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Tue Apr 27 19:51:35 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Tue Apr 27 22:21:16 2010 +0200
@@ -6,6 +6,8 @@
 
 signature NOMINAL_LIBRARY =
 sig
+
+
   val mk_minus: term -> term
   val mk_plus: term -> term -> term
 
@@ -14,6 +16,10 @@
   val mk_perm: term -> term -> term
   val dest_perm: term -> term * term
 
+  val mk_sort_of: term -> term
+  val mk_atom_ty: typ -> term -> term
+  val mk_atom: term -> term
+
   val mk_equiv: thm -> thm
   val safe_mk_equiv: thm -> thm
 end
@@ -38,9 +44,16 @@
 fun dest_perm (Const (@{const_name "permute"}, _) $ p $ t) = (p, t)
   | dest_perm t = raise TERM ("dest_perm", [t])
 
+
+fun mk_sort_of t = @{term "sort_of"} $ t;
+
+fun mk_atom_ty T t = Const (@{const_name atom}, T --> @{typ atom}) $ t;
+fun mk_atom t = mk_atom_ty (fastype_of t) t;
+
 fun mk_equiv r = r RS @{thm eq_reflection};
 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
 
+
 end (* structure *)
 
 open Nominal_Library;
\ No newline at end of file