diff -r 774d631726ad -r 84a13d1e2511 Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Tue Apr 27 19:51:35 2010 +0200
+++ b/Nominal/NewFv.thy	Tue Apr 27 22:21:16 2010 +0200
@@ -13,9 +13,8 @@
 
 ML {*
   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
-  (* TODO: It is the same as one in 'nominal_atoms' *)
-  fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom});
-  fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x];
+
+  fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom x];
   val noatoms = @{term "{} :: atom set"};
   fun mk_union sets =
     fold (fn a => fn b =>