--- a/Nominal/nominal_dt_rawfuns.ML	Sun Nov 14 16:34:47 2010 +0000
+++ b/Nominal/nominal_dt_rawfuns.ML	Mon Nov 15 01:10:02 2010 +0000
@@ -101,20 +101,20 @@
 fun mk_atom_fset t =
   let
     val ty = fastype_of t;
-    val atom_ty = dest_fsetT ty --> @{typ "atom"};
-    val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
+    val atom_ty = dest_fsetT ty
+    val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"};
     val fset = @{term "fset :: atom fset => atom set"}
   in
-    fset $ (Const (@{const_name map_fset}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
+    fset $ (Const (@{const_name map_fset}, fmap_ty) $ (atom_const atom_ty) $ t)
   end
 
   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"};
+    val ty = fastype_of t
+    val atom_ty = dest_listT ty
+    val map_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom list"}
   in
-    Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t
+    Const (@{const_name map}, map_ty) $ (atom_const atom_ty) $ t
   end
 
 (* functions that coerces singletons, sets and fsets of concrete atoms
@@ -141,14 +141,14 @@
     if is_atom ctxt ty
       then HOLogic.mk_list @{typ atom} [mk_atom t]
     else if is_atom_list ctxt ty
-      then mk_atom_set t
+      then mk_atom_list t
     else raise TERM ("listify", [t])
   end
 
 (* coerces a list into a set *)
 fun to_set t =
   if fastype_of t = @{typ "atom list"}
-  then @{term "set::atom list => atom set"} $ t
+  then @{term "set :: atom list => atom set"} $ t
   else t
 
 
@@ -272,7 +272,7 @@
 
     val (_, lthy') = Function.add_function all_fun_names all_fun_eqs
       Function_Common.default_config (pat_completeness_simp constr_thms) lthy
-  
+
     val (info, lthy'') = prove_termination size_simps (Local_Theory.restore lthy')
  
     val {fs, simps, inducts, ...} = info;