Nominal/nominal_library.ML
changeset 3245 017e33849f4d
parent 3244 a44479bde681
--- a/Nominal/nominal_library.ML	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/nominal_library.ML	Thu Apr 19 13:57:17 2018 +0100
@@ -131,7 +131,7 @@
     val atom_ty = dest_fsetT ty
     val fmap_ty = (atom_ty --> @{typ atom}) --> ty --> @{typ "atom fset"};
   in
-    Const (@{const_name map_fset}, fmap_ty) $ atom_const atom_ty $ t
+    Const (@{const_name fimage}, fmap_ty) $ atom_const atom_ty $ t
   end
 
 fun mk_atom_list_ty ty t =