diff -r 1c77e15c4259 -r f0252365936c Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Mon Nov 15 08:17:11 2010 +0000
+++ b/Nominal/nominal_library.ML	Mon Nov 15 09:52:29 2010 +0000
@@ -49,7 +49,6 @@
   val mk_finite_ty: typ -> term -> term
   val mk_finite: term -> term
 
-
   val mk_equiv: thm -> thm
   val safe_mk_equiv: thm -> thm
 
@@ -61,6 +60,8 @@
   val mk_conj: term * term -> term
   val fold_conj: term list -> term
 
+  val to_set: term -> term
+
   (* fresh arguments for a term *)
   val fresh_args: Proof.context -> term -> term list
 
@@ -185,6 +186,13 @@
 fun fold_conj trms = fold_rev (curry mk_conj) trms @{term "True"}
 
 
+(* coerces a list into a set *)
+fun to_set t =
+  if fastype_of t = @{typ "atom list"}
+  then @{term "set :: atom list => atom set"} $ t
+  else t
+
+
 (* produces fresh arguments for a term *)
 
 fun fresh_args ctxt f =