diff -r 0865caafbfe6 -r 3890483c674f Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Mon Jan 03 16:21:12 2011 +0000
+++ b/Nominal/nominal_library.ML	Tue Jan 04 13:47:38 2011 +0000
@@ -23,6 +23,7 @@
   val mk_id: term -> term
   val mk_all: (string * typ) -> term -> term
   val mk_All: (string * typ) -> term -> term
+  val mk_exists: (string * typ) -> term -> term
 
   val sum_case_const: typ -> typ -> typ -> term
   val mk_sum_case: term -> term -> term
@@ -204,6 +205,8 @@
 
 fun mk_All (a, T) t =  HOLogic.all_const T $ Abs (a, T, t)
 
+fun mk_exists (a, T) t =  HOLogic.exists_const T $ Abs (a, T, t)
+
 fun sum_case_const ty1 ty2 ty3 = 
   Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3)