--- a/Quot/Nominal/Fv.thy	Thu Feb 18 08:43:13 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Thu Feb 18 09:46:38 2010 +0100
@@ -23,6 +23,11 @@
  [],
  [[], [], [(NONE, 0)]],
  [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]]
+
+A SOME binding has to have a function returning an atom set,
+and a NONE binding has to be on an argument that is an atom
+or an atom set.
+
 *)
 
 ML {*
@@ -40,13 +45,24 @@
     if b = noatoms then a else
     if b = a then noatoms else
     HOLogic.mk_binop @{const_name minus} (a, b);
+  fun mk_atoms t =
+    let
+      val ty = fastype_of t;
+      val atom_ty = HOLogic.dest_setT ty --> @{typ atom};
+      val img_ty = atom_ty --> ty --> @{typ "atom set"};
+    in
+      (Const (@{const_name image}, img_ty) $ Const (@{const_name atom}, atom_ty) $ t)
+    end;
+  (* Copy from Term *)
+  fun is_funtype (Type ("fun", [_, _])) = true
+    | is_funtype _ = false;
 *}
 
 ML {*
 (* Currently needs just one full_tname to access Datatype *)
 fun define_raw_fv full_tname bindsall lthy =
 let
-  val thy = ProofContext.theory_of lthy
+  val thy = ProofContext.theory_of lthy;
   val {descr, ...} = Datatype.the_info thy full_tname;
   val sorts = []; (* TODO *)
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
@@ -64,6 +80,7 @@
       fun fv_bind (NONE, i) =
             if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
             (* TODO we assume that all can be 'atomized' *)
+            if (is_funtype o fastype_of) (nth args i) then mk_atoms (nth args i) else
             mk_single_atom (nth args i)
         | fv_bind (SOME f, i) = f $ (nth args i);
       fun fv_arg ((dt, x), bindxs) =
@@ -71,7 +88,8 @@
           val arg =
             if is_rec_type dt then nth fv_frees (body_index dt) $ x else
             (* TODO: we just assume everything can be 'atomized' *)
-            HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x]
+            if (is_funtype o fastype_of) x then mk_atoms x else
+            HOLogic.mk_set @{typ atom} [mk_atom (fastype_of x) $ x]
           val sub = mk_union (map fv_bind bindxs)
         in
           mk_diff arg sub
@@ -91,9 +109,18 @@
 end
 *}
 
-(* test
+(* tests:
+
 atom_decl name
 
+datatype ty =
+  Var "name set"
+
+ML {* Syntax.check_term @{context} (mk_atoms @{term "a :: name set"}) *}
+
+local_setup {* define_raw_fv "Fv.ty" [[[[]]]] *}
+print_theorems
+
 datatype rtrm1 =
   rVr1 "name"
 | rAp1 "rtrm1" "rtrm1"

--- a/Quot/Nominal/Terms.thy	Thu Feb 18 08:43:13 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Thu Feb 18 09:46:38 2010 +0100
@@ -1076,14 +1076,11 @@
 setup {* snd o define_raw_perms ["tyS"] ["Terms.tyS"] *}
 print_theorems
 
-abbreviation
-  "atoms xs \<equiv> {atom x| x. x \<in> xs}"
-
 local_setup {* define_raw_fv "Terms.ty" [[[[]], [[], []]]] *}
 print_theorems 
 
 (*
-doesn't work yet
+Doesnot work yet since we do not refer to fv_ty
 local_setup {* define_raw_fv "Terms.tyS" [[[[], []]]] *}
 print_theorems
 *)
@@ -1091,12 +1088,12 @@
 primrec
   fv_tyS
 where 
-  "fv_tyS (All xs T) = (fv_ty T - atoms xs)"
+  "fv_tyS (All xs T) = (fv_ty T - atom ` xs)"
 
 inductive
   alpha_tyS :: "tyS \<Rightarrow> tyS \<Rightarrow> bool" ("_ \<approx>tyS _" [100, 100] 100)
 where
-  a1: "\<exists>pi. ((atoms xs1, T1) \<approx>gen (op =) fv_ty pi (atoms xs2, T2)) 
+  a1: "\<exists>pi. ((atom ` xs1, T1) \<approx>gen (op =) fv_ty pi (atom ` xs2, T2)) 
         \<Longrightarrow> All xs1 T1 \<approx>tyS All xs2 T2"
 
 lemma