# HG changeset patch
# User berghofe
# Date 1222433590 -7200
# Node ID 5e2c526cfaf03a744437aa5ff0945edb0102d196
# Parent  291e7a158e957c0e85f525b344bb29734b64c1d2
Added fresh_star_const.

diff -r 291e7a158e95 -r 5e2c526cfaf0 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Fri Sep 26 14:52:27 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML	Fri Sep 26 14:53:10 2008 +0200
@@ -18,6 +18,7 @@
   val mk_not_sym: thm list -> thm list
   val perm_simproc: simproc
   val fresh_const: typ -> typ -> term
+  val fresh_star_const: typ -> typ -> term
 end
 
 structure NominalPackage : NOMINAL_PACKAGE =
@@ -189,6 +190,8 @@
   | _ => [th]) ths;
 
 fun fresh_const T U = Const ("Nominal.fresh", T --> U --> HOLogic.boolT);
+fun fresh_star_const T U =
+  Const ("Nominal.fresh_star", HOLogic.mk_setT T --> U --> HOLogic.boolT);
 
 fun gen_add_nominal_datatype prep_typ err flat_names new_type_names dts thy =
   let