--- a/Nominal/Fv.thy	Sat Mar 27 12:01:28 2010 +0100
+++ b/Nominal/Fv.thy	Sat Mar 27 12:20:17 2010 +0100
@@ -409,6 +409,12 @@
   length (distinct (op =) (map (fn ((b, _, _, atyp), _) => (b, atyp)) l)) = 1
 *}
 
+ML {*
+fun setify x =
+  if fastype_of x = @{typ "atom list"} then
+  Const (@{const_name set}, @{typ "atom list \<Rightarrow> atom set"}) $ x else x
+*}
+
 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
 ML {*
 fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall bns lthy =
@@ -439,6 +445,7 @@
     alpha_bns dt_info alpha_frees bns bns_rec
   val alpha_bn_frees = map snd bn_alpha_bns;
   val alpha_bn_types = map fastype_of alpha_bn_frees;
+
   fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
     let
       val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -464,8 +471,9 @@
             if ((is_atom_fset thy) o fastype_of) (nth args i) then mk_atom_fset (nth args i) else
             (* TODO we do not know what to do with non-atomizable things *)
             @{term "{} :: atom set"}
-        | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i);
+        | fv_bind args (SOME (f, _), i, _, _) = f $ (nth args i)
       fun fv_binds args relevant = mk_union (map (fv_bind args) relevant)
+      fun fv_binds_as_set args relevant = mk_union (map (setify o fv_bind args) relevant)
       fun find_nonrec_binder j (SOME (f, false), i, _, _) = if i = j then SOME f else NONE
         | find_nonrec_binder _ _ = NONE
       fun fv_arg ((dt, x), arg_no) =
@@ -485,7 +493,7 @@
                 @{term "{} :: atom set"};
               (* If i = j then we generate it only once *)
               val relevant = filter (fn (_, i, j, _) => ((i = arg_no) orelse (j = arg_no))) bindcs;
-              val sub = fv_binds args relevant
+              val sub = fv_binds_as_set args relevant
             in
               mk_diff arg sub
             end;