--- a/Nominal-General/nominal_library.ML	Sat Aug 28 18:15:23 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Sun Aug 29 00:09:45 2010 +0800
@@ -33,6 +33,10 @@
   val mk_supp_ty: typ -> term -> term
   val mk_supp: term -> term
 
+  val supports_const: typ -> term
+  val mk_supports_ty: typ -> term -> term -> term
+  val mk_supports: term -> term -> term
+
   val mk_equiv: thm -> thm
   val safe_mk_equiv: thm -> thm
 
@@ -43,6 +47,9 @@
   val mk_conj: term * term -> term
   val fold_conj: term list -> term
 
+  (* fresh arguments for a term *)
+  val fresh_args: Proof.context -> term -> term list
+
   (* datatype operations *)
   type cns_info = (term * typ * typ list * bool list) list
 
@@ -114,6 +121,9 @@
 fun mk_supp_ty ty t = supp_const ty $ t;
 fun mk_supp t = mk_supp_ty (fastype_of t) t;
 
+fun supports_const ty = Const (@{const_name "supports"}, [@{typ "atom set"}, ty] ---> @{typ bool});
+fun mk_supports_ty ty t1 t2 = supports_const ty $ t1 $ t2;
+fun mk_supports t1 t2 = mk_supports_ty (fastype_of t2) t1 t2;
 
 fun mk_equiv r = r RS @{thm eq_reflection};
 fun safe_mk_equiv r = mk_equiv r handle Thm.THM _ => r;
@@ -142,6 +152,18 @@
 
 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"}
 
+
+(* produces fresh arguments for a term *)
+
+fun fresh_args ctxt f =
+    f |> fastype_of
+      |> binder_types
+      |> map (pair "z")
+      |> Variable.variant_frees ctxt [f]
+      |> map Free
+
+
+
 (** datatypes **)
 
 (* constructor infos *)