--- a/Nominal/nominal_library.ML	Sun Dec 12 22:09:11 2010 +0000
+++ b/Nominal/nominal_library.ML	Tue Dec 14 14:23:40 2010 +0000
@@ -16,6 +16,7 @@
   val dest_fsetT: typ -> typ
 
   val mk_id: term -> term
+  val mk_all: (string * typ) -> term -> term
 
   val size_const: typ -> term 
 
@@ -154,6 +155,8 @@
     Const (@{const_name id}, ty --> ty) $ trm
   end
 
+fun mk_all (a, T) t =  Term.all T $ Abs (a, T, t)
+
 
 fun size_const ty = Const (@{const_name size}, ty --> @{typ nat})