# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1338224586 -3600
# Node ID c25e4c9481f2c629b5e76c220cb2da6149fa822b
# Parent  31372760c2fb2dc322d7075fb3e3c660cd9266d7
added library routines for the constant fresh

diff -r 31372760c2fb -r c25e4c9481f2 Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Fri May 25 15:46:48 2012 +0100
+++ b/Nominal/nominal_library.ML	Mon May 28 18:03:06 2012 +0100
@@ -34,6 +34,11 @@
   val listify_ty: Proof.context -> typ -> term -> term
   val listify: Proof.context -> term -> term
 
+  val fresh_ty: typ -> typ
+  val fresh_const: typ -> term
+  val mk_fresh_ty: typ -> term -> term -> term
+  val mk_fresh: term -> term -> term
+
   val fresh_star_ty: typ -> typ
   val fresh_star_const: typ -> term
   val mk_fresh_star_ty: typ -> term -> term -> term
@@ -201,6 +206,11 @@
 fun setify ctxt t  = setify_ty ctxt (fastype_of t) t
 fun listify ctxt t = listify_ty ctxt (fastype_of t) t
 
+fun fresh_ty ty = [@{typ atom}, ty] ---> @{typ bool}
+fun fresh_const ty = Const (@{const_name fresh}, fresh_ty ty)
+fun mk_fresh_ty ty t1 t2 = fresh_const ty $ t1 $ t2
+fun mk_fresh t1 t2 = mk_fresh_ty (fastype_of t2) t1 t2
+
 fun fresh_star_ty ty = [@{typ "atom set"}, ty] ---> @{typ bool}
 fun fresh_star_const ty = Const (@{const_name fresh_star}, fresh_star_ty ty)
 fun mk_fresh_star_ty ty t1 t2 = fresh_star_const ty $ t1 $ t2