diff -r 6b51117b8955 -r 217ef3e4282e Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Sun Aug 29 00:36:47 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Sun Aug 29 01:17:36 2010 +0800
@@ -37,6 +37,11 @@
   val mk_supports_ty: typ -> term -> term -> term
   val mk_supports: term -> term -> term
 
+  val finite_const: typ -> term
+  val mk_finite_ty: typ -> term -> term
+  val mk_finite: term -> term
+
+
   val mk_equiv: thm -> thm
   val safe_mk_equiv: thm -> thm
 
@@ -117,14 +122,19 @@
 
 
 fun supp_ty ty = ty --> @{typ "atom set"};
-fun supp_const ty = Const (@{const_name "supp"}, supp_ty ty)
+fun supp_const ty = Const (@{const_name supp}, supp_ty ty)
 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 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 finite_const ty = Const (@{const_name finite}, ty --> @{typ bool})
+fun mk_finite_ty ty t = finite_const ty $ t
+fun mk_finite t = mk_finite_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;