diff -r e903c32ec24f -r 693562f03eee Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Wed Oct 13 22:55:58 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Thu Oct 14 04:14:22 2010 +0100
@@ -99,9 +99,9 @@
     val ty = fastype_of t;
     val atom_ty = dest_fsetT ty --> @{typ "atom"};
     val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
-    val fset_to_set = @{term "fset_to_set :: atom fset => atom set"}
+    val fset = @{term "fset :: atom fset => atom set"}
   in
-    fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
+    fset $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
   end
 
   fun mk_atom_list t =