Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/nominal_dt_rawfuns.ML
changeset 2542 1f5c8e85c41f
parent 2524 693562f03eee
child 2560 82e37a4595c7 
--- 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 =
nominal2