diff -r 4444d52201dc -r 45721f92e471 Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Thu Apr 29 16:18:38 2010 +0200
+++ b/Nominal/NewFv.thy	Thu Apr 29 16:59:33 2010 +0200
@@ -60,7 +60,28 @@
 *}
 
 ML {*
-fun atoms thy t =
+fun is_atom_list (Type (@{type_name list}, [T])) = true
+  | is_atom_list _ = false
+*}
+
+ML {*
+fun dest_listT (Type (@{type_name list}, [T])) = T
+  | dest_listT T = raise TYPE ("dest_listT: list type expected", [T], [])
+*}
+
+ML {*
+fun mk_atom_list t =
+let
+  val ty = fastype_of t;
+  val atom_ty = dest_listT ty --> @{typ atom};
+  val map_ty = atom_ty --> ty --> @{typ "atom list"};
+in
+  (Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t)
+end;
+*}
+
+ML {*
+fun setify thy t =
 let
   val ty = fastype_of t;
 in
@@ -70,12 +91,25 @@
     then mk_atom_set t
   else if is_atom_fset thy ty
     then mk_atom_fset t
-  else noatoms
+  else error ("setify" ^ (PolyML.makestring (t, ty)))
 end
 *}
 
 ML {*
-fun setify x =
+fun listify thy t =
+let
+  val ty = fastype_of t;
+in
+  if is_atom thy ty
+    then HOLogic.mk_list @{typ atom} [mk_atom t]
+  else if is_atom_list ty
+    then mk_atom_set t
+  else error "listify"
+end
+*}
+
+ML {*
+fun set x =
   if fastype_of x = @{typ "atom list"}
   then @{term "set::atom list \<Rightarrow> atom set"} $ x
   else x
@@ -89,7 +123,7 @@
 in
   if Datatype_Aux.is_rec_type dt
   then nth fv_frees (Datatype_Aux.body_index dt) $ x
-  else (if supp then mk_supp x else atoms thy x)
+  else (if supp then mk_supp x else setify thy x)
 end
 *}
 
@@ -99,7 +133,7 @@
   val fv_bodys = mk_union (map (fv_body thy dts args fv_frees true) bodys)
   val bound_vars =
     case binds of
-      [(SOME bn, i)] => setify (bn $ nth args i)
+      [(SOME bn, i)] => set (bn $ nth args i)
     | _ => mk_union (map (fv_body thy dts args fv_frees false) (map snd binds));
   val non_rec_vars =
     case binds of