diff -r 7430e07a5d61 -r 86e3b39c2a60 Nominal/nominal_library.ML
--- a/Nominal/nominal_library.ML	Sun Dec 12 00:10:40 2010 +0000
+++ b/Nominal/nominal_library.ML	Sun Dec 12 22:09:11 2010 +0000
@@ -8,6 +8,7 @@
 sig
   val last2: 'a list -> 'a * 'a
   val order: ('a * 'a -> bool) -> 'a list -> ('a * 'b) list -> 'b list
+  val remove_dups: ('a * 'a -> bool) -> 'a list -> 'a list
 
   val is_true: term -> bool
  
@@ -47,14 +48,18 @@
   val is_atom_fset: Proof.context -> typ -> bool
   val is_atom_list: Proof.context -> typ -> bool
 
+  val to_atom_set: term -> term
+  val to_set_ty: typ -> term -> term
+  val to_set: term -> term
+  
   val setify_ty: Proof.context -> typ -> term -> term
   val setify: Proof.context -> term -> term
   val listify_ty: Proof.context -> typ -> term -> term
   val listify: Proof.context -> term -> term
 
-  val fresh_ty: typ -> typ -> typ
-  val fresh_star_const: typ -> typ -> term
-  val mk_fresh_star_ty: typ -> typ -> term -> term -> term
+  val fresh_star_ty: typ -> typ
+  val fresh_star_const: typ -> term
+  val mk_fresh_star_ty: typ -> term -> term -> term
   val mk_fresh_star: term -> term -> term
 
   val supp_ty: typ -> typ
@@ -86,8 +91,6 @@
   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
 
@@ -121,6 +124,13 @@
 fun order eq keys list = 
   map (the o AList.lookup eq list) keys
 
+fun remove_dups eq [] = []
+  | remove_dups eq (x::xs) = 
+      if (member eq xs x) 
+      then remove_dups eq xs 
+      else x::(remove_dups eq xs)
+
+
 fun last2 [] = raise Empty
   | last2 [_] = raise Empty
   | last2 [x, y] = (x, y)
@@ -206,19 +216,27 @@
 fun mk_atom_fset t = mk_atom_fset_ty (fastype_of t) t
 fun mk_atom_list t = mk_atom_list_ty (fastype_of t) t
 
+(* coerces a list into a set *)
+fun to_atom_set t = @{term "set :: atom list => atom set"} $ t
+  
+fun to_set_ty ty t =
+  if ty = @{typ "atom list"}
+  then to_atom_set t else t
+
+fun to_set t = to_set_ty (fastype_of t) t
 
 
 (* testing for concrete atom types *)
 fun is_atom ctxt ty =
   Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
 
-fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
+fun is_atom_set ctxt (Type ("fun", [ty, @{typ bool}])) = is_atom ctxt ty
   | is_atom_set _ _ = false;
 
-fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
+fun is_atom_fset ctxt (Type (@{type_name "fset"}, [ty])) = is_atom ctxt ty
   | is_atom_fset _ _ = false;
 
-fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
+fun is_atom_list ctxt (Type (@{type_name "list"}, [ty])) = is_atom ctxt ty
   | is_atom_list _ _ = false
 
 
@@ -231,8 +249,11 @@
     then mk_atom_set_ty ty t
   else if is_atom_fset ctxt ty
     then mk_atom_fset_ty ty t
+  else if is_atom_list ctxt ty
+    then to_atom_set (mk_atom_list_ty ty t)
   else raise TERM ("setify", [t])
 
+
 (* functions that coerces singletons and lists of concrete atoms
    into lists of general atoms  *)
 fun listify_ty ctxt ty t =
@@ -245,10 +266,10 @@
 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 ty1 ty2 = [ty1, ty2] ---> @{typ bool}
-fun fresh_star_const ty1 ty2 = Const (@{const_name fresh_star}, fresh_ty ty1 ty2)
-fun mk_fresh_star_ty ty1 ty2 t1 t2 = fresh_star_const ty1 ty2 $ t1 $ t2
-fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t1) (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
+fun mk_fresh_star t1 t2 = mk_fresh_star_ty (fastype_of t2) t1 t2
 
 fun supp_ty ty = ty --> @{typ "atom set"};
 fun supp_const ty = Const (@{const_name supp}, supp_ty ty)
@@ -302,15 +323,6 @@
 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 =