diff -r d7269488c4b5 -r 1f5c8e85c41f Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Sun Oct 17 15:28:05 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Sun Oct 17 15:53:37 2010 +0100
@@ -101,7 +101,7 @@
     val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
     val fset = @{term "fset :: atom fset => atom set"}
   in
-    fset $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
+    fset $ (Const (@{const_name map_fset}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
   end
 
   fun mk_atom_list t =