--- a/Nominal-General/nominal_library.ML	Thu Apr 29 10:59:08 2010 +0200
+++ b/Nominal-General/nominal_library.ML	Thu Apr 29 11:00:18 2010 +0200
@@ -1,13 +1,11 @@
 (*  Title:      nominal_library.ML
     Author:     Christian Urban
 
-  Basic function for nominal.
+  Basic functions for nominal.
 *)
 
 signature NOMINAL_LIBRARY =
 sig
-
-
   val mk_minus: term -> term
   val mk_plus: term -> term -> term
 
@@ -17,9 +15,14 @@
   val dest_perm: term -> term * term
 
   val mk_sort_of: term -> term
+  val atom_ty: typ -> typ
   val mk_atom_ty: typ -> term -> term
   val mk_atom: term -> term
 
+  val supp_ty: typ -> typ
+  val mk_supp_ty: typ -> term -> term
+  val mk_supp: term -> term
+
   val mk_equiv: thm -> thm
   val safe_mk_equiv: thm -> thm
 end
@@ -28,27 +31,30 @@
 structure Nominal_Library: NOMINAL_LIBRARY =
 struct
 
-fun mk_minus p = 
- @{term "uminus::perm => perm"} $ p
+fun mk_minus p = @{term "uminus::perm => perm"} $ p;
+
+fun mk_plus p q = @{term "plus::perm => perm => perm"} $ p $ q;
 
-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"}, perm_ty ty) $ p $ trm
-fun mk_perm p trm = mk_perm_ty (fastype_of trm) p trm
+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)
-  | dest_perm t = raise TERM ("dest_perm", [t])
+  | dest_perm t = raise TERM ("dest_perm", [t]);
 
 
 fun mk_sort_of t = @{term "sort_of"} $ t;
 
-fun atom_ty ty = ty --> @{typ "atom"}
+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 supp_ty ty = ty --> @{typ "atom set"};
+fun mk_supp_ty ty t = Const (@{const_name "supp"}, supp_ty ty) $ t;
+fun mk_supp t = mk_supp_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;