--- a/Nominal/nominal_library.ML	Sun Nov 14 16:34:47 2010 +0000
+++ b/Nominal/nominal_library.ML	Mon Nov 15 01:10:02 2010 +0000
@@ -27,6 +27,7 @@
 
   val mk_sort_of: term -> term
   val atom_ty: typ -> typ
+  val atom_const: typ -> term
   val mk_atom_ty: typ -> term -> term
   val mk_atom: term -> term
 
@@ -128,10 +129,10 @@
 fun mk_sort_of t = @{term "sort_of"} $ t;
 
 fun atom_ty ty = ty --> @{typ "atom"};
-fun mk_atom_ty ty t = Const (@{const_name "atom"}, atom_ty ty) $ t;
+fun atom_const ty = Const (@{const_name "atom"}, atom_ty ty)
+fun mk_atom_ty ty t = atom_const ty $ t;
 fun mk_atom t = mk_atom_ty (fastype_of t) t;
 
-
 fun supp_ty ty = ty --> @{typ "atom set"};
 fun supp_const ty = Const (@{const_name supp}, supp_ty ty)
 fun mk_supp_ty ty t = supp_const ty $ t