Added fresh_star_const.

--- 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