diff -r d1b4c4a28c99 -r 4538d63ecc9b Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Thu Apr 29 11:00:18 2010 +0200
+++ b/Nominal/NewFv.thy	Thu Apr 29 11:54:39 2010 +0200
@@ -64,45 +64,40 @@
 let
   val ty = fastype_of t;
 in
-  if is_atom thy ty 
-    then mk_singleton_atom t 
-  else if is_atom_set thy ty 
-    then mk_atom_set t 
-  else if is_atom_fset thy ty 
-    then mk_atom_fset t 
+  if is_atom thy ty
+    then mk_singleton_atom t
+  else if is_atom_set thy ty
+    then mk_atom_set t
+  else if is_atom_fset thy ty
+    then mk_atom_fset t
   else noatoms
 end
 *}
 
 ML {*
-fun mk_supp t =
-  Const (@{const_name supp}, fastype_of t --> @{typ "atom set"}) $ t
-*}
-
-ML {*
 fun setify x =
-  if fastype_of x = @{typ "atom list"} 
-  then @{term "set::atom list \<Rightarrow> atom set"} $ x 
+  if fastype_of x = @{typ "atom list"}
+  then @{term "set::atom list \<Rightarrow> atom set"} $ x
   else x
 *}
 
 ML {*
 fun fv_bm_lsts thy dts args fv_frees bn_fvbn binds bodys =
 let
-  fun fv_body i =
+  fun fv_body supp i =
     let
       val x = nth args i;
       val dt = nth dts i;
     in
       if Datatype_Aux.is_rec_type dt
       then nth fv_frees (Datatype_Aux.body_index dt) $ x
-      else mk_supp x
+      else (if supp then mk_supp x else atoms thy x)
     end
-  val fv_bodys = mk_union (map fv_body bodys)
+  val fv_bodys = mk_union (map (fv_body true) bodys)
   val bound_vars =
     case binds of
       [(SOME bn, i)] => setify (bn $ nth args i)
-    | _ => mk_union (map fv_body (map snd binds));
+    | _ => mk_union (map (fv_body false) (map snd binds));
   val non_rec_vars =
     case binds of
       [(SOME bn, i)] =>